How do you see where identifiers are defined in Coq efficiently?

Question

In most IDEs or text editors, you can right-click the term and it will lead you to the file in which the term is defined. CoqIDE doesn't seem to have this, so I did coqdoc myfile.v --htmland then moved on to the generated HTML documents. But the only clickable conditions for this file are for the Coq standard library. Terms defined by ssreflect (for example) are not clickable.

Is there a standard way to quickly search when a specific member / identifier is defined (and the source code for it) when in a Coq file? Either in CoqIDE or in emacs + ProofGeneral (I use CoqIDE, but I would switch if emacs / ProofGeneral had this ability).

Or the standard way to create documents for each Coq project and the dependency you use?

Answer 1

If you select the term and do Queries → Find, or you evaluate Locate some_identifier., you will get the full name of the constant. If you know where the dependencies are installed, this will tell you where to look for the identifier.

Edit: if you want to define an identifier, you can have Printit. If you just want its type, you can use Aboutor Check(which also accepts expressions, not just identifiers).

Answer 2

, Proof General, company-coq. , M-. .

( ), , , Require .