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 extensions.
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional last column (not currently used but was in the past).
- D. _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
