Tom Prince <tom.pri...@ualberta.net> writes: > Some developments don't fully qualify their imports, and so coqdep gives > warning about ambiguous imports. Allow these developments to use > auto-compilation mode anyway.
Sorry about the delay, I somehow forgot about the issue. It's now fixed in the repository. The regular expression for detecting coqdep errors can be customized now and the default value is chosen more carefully to only match those cases where a library cannot be found. If you really want to ignore all warnings you can change coq-coqdep-error-regexp such that if will never match anything. But be prepared to hit the assertion in coq-map-module-id-to-obj-file, when you ignore the "library X is required and has not been found" warning for a require command. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
