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 <tom.pri...@ualberta.net>
---
 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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to