Has anyone worked on a tool to generate tag files for Coq (like what ctags
creates)? The .glob files look promising, but I think I remember seeing somewhere that their format isn't fixed across versions and shouldn't be relied on? What does coqdoc
use to create links to where things are defined?
I believe it uses the glob
files. @Jason Gross also uses this for his bug minimizer. I think the format is somewhat stable.
We use etags in HoTT
https://github.com/HoTT/HoTT/blob/master/INSTALL.md#41-tags-for-emacs
I just wrote a universal-ctags configuration for coq. https://github.com/tomtomjhj/coq.ctags
Last updated: Dec 01 2023 at 06:01 UTC