From f86882c6352c97753f74883cfeb4f17dab8d2f34 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 11 Mar 2004 13:24:33 +0000
Subject: added proof-really-save-command-p to coq config, to deal with Proof
 <term>. which is a save command (but not a save giving a name like Save id.).

---
 coq/coq-syntax.el | 16 ++++++++++++----
 coq/coq.el        |  1 +
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 06b5897a..82d13924 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -230,7 +230,9 @@ of STRG matching REGEXP. Empty match are counted once."
   )
 
 
-(defvar coq-keywords-save
+
+
+(defvar coq-keywords-save-strict
   '("Defined"
     "Save"
     "Qed"
@@ -238,9 +240,13 @@ of STRG matching REGEXP. Empty match are counted once."
 	 "Admitted"
 	 ))
 
-(defun coq-save-command-p (str)
+(defvar coq-keywords-save
+  (append coq-keywords-save-strict '("Proof"))
+)
+
+(defun coq-save-command-p (span str)
   "Decide whether argument is a Save command or not"
-  (or (proof-string-match coq-save-command-regexp str)
+  (or (proof-string-match coq-save-command-regexp-strict str)
 		(and (proof-string-match "\\`Proof\\>" str)
 			  (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str)))
 		)
@@ -735,10 +741,12 @@ Idtac (Nop) tactic, put the following line in your .emacs:
 ;; According to Coq, "Definition" is both a declaration and a goal.
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
+(defconst coq-save-command-regexp-strict
+  (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save-strict)))
 (defconst coq-save-command-regexp
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save)))
 (defconst coq-save-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp coq-keywords-save)
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-save-strict)
 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\."))
 (defconst coq-goal-command-regexp
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal)))
diff --git a/coq/coq.el b/coq/coq.el
index bea485be..867d8fd5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -758,6 +758,7 @@ This is specific to coq-mode."
 	proof-state-preserving-p 'coq-state-preserving-p)
 
   (setq proof-save-command-regexp coq-save-command-regexp
+        proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>.
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
 	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
 	proof-nested-undo-regexp coq-state-changing-commands-regexp)
-- 
cgit v1.2.3