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.

Could you describe an example? What is coqdep printing in these

   -    (if (string-match "^\\*\\*\\* Warning" coqdep-output)
   +    (if (and (not coq-auto-compilation-ignore-coqdep-warnings)
   +             (string-match "^\\*\\*\\* Warning" coqdep-output))

I would rather prefer to change the regular expression here, in
order to only ignore the warning about ambiguous imports.


ProofGeneral-devel mailing list

Reply via email to