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.
I suppose you are right, it should be set early and it makes sense to
put in proof-assistant-table because that configures the main file name
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional
last column (not currently used but was in the past).
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.