Added a file for testing modules of coq (new version 7.4). Plus some

modification to better backtrack modules.

3 files changed, 72 insertions, 8 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 201cfca1..f0daec25 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -152,8 +152,8 @@
    (t '("Section"))))
 
 (defvar coq-section-regexp 
-;  (proof-ids-to-regexp coq-keywords-section)
-  "\\(\\<Section\\>\\|\\<Module\\>\\-+\\<Type\\>\\|\\<Module\\>\\)"
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-section) "\\)")
+;  "\\(\\<Section\\>\\|\\<Module\\>\\-+\\<Type\\>\\|\\<Module\\>\\)"
 )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -210,7 +210,8 @@
   "Decide whether argument is a goal or not"
   (and (proof-string-match coq-goal-command-regexp str)
        (not (proof-string-match "Definition.*:=" str))
-		 (not (proof-string-match "Recursive Definition" str))
+       (not (proof-string-match "Module.*:=" str))
+       (not (proof-string-match "Recursive Definition" str))
        ;; da: 3.4 test: do not exclude Lemma: we want goal-command-p to
        ;; succeed for nested goals too now.
        ;; (should we also exclude Definition?)
@@ -245,7 +246,18 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
       (setq str (span-property span 'cmd))
       (cond
        ((eq (span-property span 'type) 'comment))
-       
+       ;; One more particular case (7.4, coq raise an error if < 7.4): 
+       ;; Module <Type> T ... :=... . inside proof (shoul perhaps been disallowed in coq)
+       ;; Should behave like Definition ... :=... . (ie no proof started, and no section-like started)
+       ;; Should go in last cond, but I have a problem trying to avoid next cond to match.
+       ((and (coq-proof-mode-p) (proof-string-match "\\(\\<Module\\>\\).*:=" str))
+        (incf nbacks))
+       ;; this case is correctly treated by the next 
+       ;; one because 'Module :=' is not a 'goalsave span
+       ;((and (not (coq-proof-mode-p)) 
+       ;      (proof-string-match 
+       ;       (concat "\\(\\<Module\\>\\)\\s-+\\(" proof-id "\\).*:=") str))
+       ; (setq ans (format coq-forget-id-command (match-string 2 str))))
        ;; FIXME: combine with coq-keywords-decl-defn-regexp case below?
        ;; [ Maybe not: Section is being treated as a _goal_ command
        ;;   now, so this test has to appear before the goalsave ]       
@@ -264,8 +276,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
         (if (equal (match-string 2 str) "Type") ;Module Type id: take the third word
             (progn 
               (setq ans (format coq-forget-id-command (match-string 5 str))))
-          (setq ans (format coq-forget-id-command (match-string 2 str))))
-        )
+          (setq ans (format coq-forget-id-command (match-string 2 str)))))
        ((eq (span-property span 'type) 'goalsave)
         ;; Note da 6.10.99: in Lego and Isabelle, it's trivial to forget an
         ;; unnamed theorem.  Coq really does use the identifier
@@ -281,7 +292,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
        ;; Unsaved goal commands: each time we hit one of these
        ;; we need to issue Abort to drop the proof state.
        ((coq-goal-command-p str)
-        ;;Todo Hack: if Definition:foo. inside a "Module Type": it is
+        ;;TODO if Definition:foo. inside a "Module Type": it is
         ;;not a proof start!!
         ;(if (and (proof-string-match "Definition\\-+:[^=]?" str)
         ;         (inside-module-type))
diff --git a/coq/ex-module.v b/coq/ex-module.v
new file mode 100644
index 00000000..e9d42072
--- /dev/null
+++ b/coq/ex-module.v
@@ -0,0 +1,49 @@
+
+Module M.
+  Module Type SIG.
+    Parameter T:Set.
+    Parameter x:T.
+  End SIG.
+  Module N:SIG.
+    Definition T:=nat.
+    Definition x:=O.
+  End N.
+End M.
+
+Section toto.
+Print M.
+End toto.
+
+
+Lemma toto : O=O.
+Module N:=M.
+Definition t:=M.N.T.
+Trivial.
+Save.
+
+
+Module Type SPRYT.
+  Module N.
+    Definition T:=M.N.T.
+    Parameter x:T.
+  End N.
+End SPRYT.
+
+Module K:SPRYT:=N.  
+Module K':SPRYT:=M.  
+
+Lemma titi : O=O.
+Module Type S:=SPRYT.
+Module N':=M.
+Trivial.
+Save.
+
+
+Module Type SIG.
+  Definition T:Set:=M.N.T.
+  Parameter x:T.
+
+  Module N:SPRYT.
+End SIG.
+
+Module J:M.SIG:=M.N.
diff --git a/coq/example.v b/coq/example.v
index 5d55a2ae..6f92e279 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -9,7 +9,7 @@
     $Id$
 *)
 
-Section sect.
+Module sect.
 
 Goal (A,B:Prop)(A /\ B) -> (B /\ A).
  Intros A B H.
@@ -32,5 +32,9 @@ End mod.
 
 Module Type newmod.
 Definition type1:=Set.
+
+Goal (n:nat)n=n.
+Auto.
+Save toto.
 End newmod.