>But admittedly, it also means that it's mostly useless as well: if your
>Coq file is called ".v" the completion will stop at ".v" in any case,
> No, it won't, because Coq does also generate ".glob" files.
Indeed adding the .glob extension would be useful, contrary to the .vo
I was talking
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional
last column (not currently used but was in the past).
Just committed.
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailm
