Stefan Monnier writes:
   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,

No, it won't, because Coq does also generate ".glob" files.
Additionally completion-ignored-extensions are hidden by default
in dired buffers.

ProofGeneral-devel mailing list

Reply via email to