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
to completion-ignored-extensions.


ProofGeneral-devel mailing list

Reply via email to