How do you look up where identifiers are defined in Coq efficiently?

Question

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then going to the generated HTML docs. But the only clickable terms in that file are for Coq Standard Library. Terms defined by ssreflect (for example) aren't clickable.

Is there a standard way to be able to quickly lookup where some term/identifier is defined (and the source code for it) when in a Coq file? Either in the CoqIDE or in emacs + ProofGeneral (I'm using CoqIDE, but I'd switch if emacs/ProofGeneral had this ability).

Or is the standard way to generate docs for every Coq project and dependency you use?

Answer 1

If you highlight a term, and do Queries -> Locate, 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 the definition of the identifier, you can Print it. If you just want it's type, you can use About, or Check (which also accepts expressions, and not just identifiers).

Answer 2

There is a tool working on top of Proof General, called company-coq. It has the jump to definition feature bound to the M-. keyboard shortcut by default.

It can jump to the definition under cursor (even to the standard library) only if the module containing the definition is required with Require command or its variant.