Tom Prince <> 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.


ProofGeneral-devel mailing list

Reply via email to