Browse definition in Coq-IDE

Question

In the Isabelle proof assistant, one can click Ctrl+click on a term and the IDE redirects him to the relevant definition.

Can this be done with CoqIde? With Proof-General?

Answer 1

Yes, the features you mention in your post and in your comment (as an aside, feel free to edit your question to incorporate your comment) are possible in Proof-General and/or company-coq (an Emacs package gathering IDE extensions of Proof-General):

• to see the content of a definition def (equivalent of Print def.): C-c C-a C-p def RET
• to see the type of a definition def (equivalent of Check def.): C-c C-a C-c def RET
• to see the type and related metadata of a definition def (equivalent of About def.): C-c C-a C-b def RET
• to see all this in one go for the identifier under point (requires company-coq): C-c C-d
• to be redirected to the location of the definition under point (requires company-coq): M-.
• to make the definition under point show up without moving (requires company-coq): <C-down-mouse-1>

Reminders

Just to be self-contained, the Emacs keybindings C-c, M-., RET, <C-down-mouse-1> refer to Ctrl+c, Alt+., Return, and Ctrl+click (without releasing the mouse button).

Finally you can discover the list of bindings associated to the ambient mode by doing C-h m:

C-h k [describe-key] C-h m [describe-mode]:

C-h m runs the command describe-mode (found in global-map), which is
an interactive compiled Lisp function in ‘help.el’.

It is bound to C-h m, <f1> m, <help> m, <menu-bar> <help-menu>
<describe> <describe-mode>.

(describe-mode &optional BUFFER)

Display documentation of current major mode and minor modes.
A brief summary of the minor modes comes first, followed by the
major mode description.  This is followed by detailed
descriptions of the minor modes, each on a separate page.

[…]