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. Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
