>> 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.
> Much neater idea... although at the moment our autoloads are only generated
> for the generic code and one might hope that e.g. using Isabelle doesn't
> automatically make .vo files unreadable -- in case Isabelle would use that
> extension for something else (it probably doesn't, but).
completion-ignored-extensions only tells completion to prefer files with
other extensions. So you can still read those files just fine if you
don't rely too heavily on completion. They even still appear in
*Completions*. So it's usually pretty harmless.
But admittedly, it also means that it's mostly useless as well: if your
Coq file is called ".v" the completion will stop at ".v" in any case,
regardless of whether you have a .vo file or not and if you've added .vo
to completion-ignored-extensions. The only case where it would make
a difference is when you have a .v8 file (or some such extension) where
the presence of a .vo might cause completion of "foo" to stop at "foo.v"
rather than go all the way to "foo.v8".
ProofGeneral-devel mailing list