`M-.` and notations

[vzaliva]

Consider the following code:

Definition foo := unit.
Notation bar := foo.
Lemma FooBar: foo = bar.

In edit buffer positioning the cursor on bar in the goal and pressing M-. jumps to the definition of bar notation.
Doing the same in the *goals* buffer triggers an error: "No location found for 'bar'".

Coq 8.11.2 (via opam)
GNU Emacs 26.3 (build 2, x86_64-pc-linux-gnu, GTK+ Version 3.22.30) of 2019-09-16
Compan-coq Version: 20200625.1650 (via MELPA)

[cpitclaudel]

Thanks, the bug is here:

(defun company-coq-library-path (lib-path mod-name fallback-spec)
  "Find a .v file likely to hold the definition of (LIB-PATH MOD-NAME).
May also return a buffer visiting that file.  FALLBACK-SPEC is a
module path specification to be used if [Locate Library] points
to a non-existent file (for an example of such a case, try
\[Locate Library Peano] in 8.4pl3)."
  (if (and (equal lib-path "")
           (or (equal mod-name "Top")
               (and buffer-file-name
                    (equal (concat mod-name ".v")
                           (file-name-nondirectory buffer-file-name)))))
      (current-buffer)
    (let* ((lib-name (concat lib-path mod-name))
           (output   (company-coq-ask-prover-swallow-errors (format company-coq-locate-lib-cmd lib-name))))
      (or (and output (save-match-data
                        (when (and (string-match company-coq-locate-lib-output-format output)
                                   (string-match-p company-coq-compiled-regexp (match-string-no-properties 3 output)))
                          (concat (match-string-no-properties 2 output) ".v"))))
          (and fallback-spec (expand-file-name (concat mod-name ".v") (cdr fallback-spec)))))))

This part:

  (if (and (equal lib-path "")
           (or (equal mod-name "Top")
               (and buffer-file-name
                    (equal (concat mod-name ".v")
                           (file-name-nondirectory buffer-file-name)))))
      (current-buffer)

should not return current-buffer, it should return the current proof buffer (otherwise we look for the definition in the goals buffer).