Requesting support for .vos (in addition to .vio) files
yoichi-at-bedrock opened this issue · 2 comments
yoichi-at-bedrock commented
Currently, M-. on a library name doesn't work for libraries found in .vos files (it works when the library is found in a .vo file).
Perhaps company-coq-compiled-regexp can be modified to allow .vos suffix?
Blaisorblade commented
23b849a (from 2015!) suggests this should be easy-ish.
cpitclaudel commented
Indeed, it should be relatively easy to add support for vos. I'm old school, so I haven't actually used them, but I'd be happy to merge a PR.