> 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.
As Emacs maintainer I recommend package maintainers to setup their
"foo-site.el" such that it is (mostly if not completely) auto-generated
by something like update-directory-autoloads.
In such a situation a simple
(add-to-list 'completion-ignored-extensions ".vo")
in coq.el will do the trick.
ProofGeneral-devel mailing list