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