David Aspinall <david.aspin...@ed.ac.uk> writes:
Hendrik, do you want to add this for Coq?
Yes, as soon as we agree on how to it best.
I don't think it needs to
be added to generic mechanisms since Coq is the only supported prover
that compiles files at the moment.
You are right. However, completion-ignored-extensions should be
set up _before_ visiting the first Coq file. That is, it must be
initialized when Emacs loads proof-site.el. As far as I can see
the only prover specific stuff, which proof-site.el does, comes
from proof-assistant-table. Therefore I suggested, to extend
proof-assistant-table with one row for ignored extensions. This
is not particularly nice, because Coq will be the only one that
uses this row.
If you don't like changing proof-assistant-table, my suggestion
is the following: In proof-site.el I add a new defcustom
proof-general-completion-ignored-extensions with default value
'(".vo" ".glob"). Additionally, somewhere in proof-site.el the
contents of proof-general-completion-ignored-extensions is added
ProofGeneral-devel mailing list