diff options
| -rw-r--r-- | coq/coq.el | 25 | ||||
| -rw-r--r-- | coq/ex-module.v | 49 | ||||
| -rw-r--r-- | coq/example.v | 6 |
3 files changed, 72 insertions, 8 deletions
@@ -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. |