Company-coq lets you jump to definition with
M-. (or with
, g g in spacemacs's coq layer), but how do you jump back? I don't see
M-, working... Probably spacemacs interferes, but docs don't seem to mention it?
I don't know the Company-coq way, but if you happen to use vim keybindings, you can use
Ctrl+o to jump back to where you were (and
Ctrl+i to more forward).
I think this
M-. uses the standard mark ring infrastructure to save the previous location. So you can jump back with
pop-global-mark. For me, this is bound to
Last updated: Feb 06 2023 at 06:29 UTC