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
I just wrote a universal-ctags configuration for coq. https://github.com/tomtomjhj/coq.ctags
Last updated: Feb 05 2023 at 07:03 UTC