> 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

Reply via email to