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