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.
Signed-off-by: Tom Prince <[email protected]> --- ProofGeneral-4.1RC4/coq/coq.el | 5 ++++- 1 files changed, 4 insertions(+), 1 deletions(-) diff --git a/ProofGeneral-4.1RC4/coq/coq.el b/ProofGeneral-4.1RC4/coq/coq.el index 34d0529..be7d38c 100644 --- a/ProofGeneral-4.1RC4/coq/coq.el +++ b/ProofGeneral-4.1RC4/coq/coq.el @@ -1373,6 +1373,8 @@ identifier and should therefore not be matched by this regexp.") (defvar coq-debug-auto-compilation nil "*Display more messages during compilation") +(defvar coq-auto-compilation-ignore-coqdep-warnings nil + "Ignore warning generated by coqdep.") ;; basic utilities @@ -1566,7 +1568,8 @@ break." (setq coqdep-output (buffer-string))) (if coq-debug-auto-compilation (message "coqdep output on %s: %s" lib-src-file coqdep-output)) - (if (string-match "^\\*\\*\\* Warning" coqdep-output) + (if (and (not coq-auto-compilation-ignore-coqdep-warnings) + (string-match "^\\*\\*\\* Warning" coqdep-output)) (let* ((this-command (cons coq-dependency-analyzer coqdep-arguments)) (full-command (if command-intro (cons command-intro this-command) -- 1.7.6.1 _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
