From 20f205b75f0de1de10d31196256d143c8031447c Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 24 Nov 2000 14:26:50 +0000
Subject: Add a little change to coq-find-and-forget to work better

---
 coq/coq.el | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 43a4159a..de3a261b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -148,7 +148,7 @@
 ;; FIXME Papageno 05/1999: must take sections in account.
 ;;
 ;; Pierre modified the test with proof-string-match, this way new tactics
-;; ca be undone (I also added "(*" in not-undoable-commands)
+;; can be undone (I also added "(*" in not-undoable-commands)
 (defun coq-count-undos (span)
   "Count number of undos in a span, return the command needed to undo that far."
   (let ((ct 0) str i)
@@ -224,9 +224,11 @@
 
        ;; If it's not a goal but it contains "Definition" then it's a
        ;; declaration
+       ;; Pierre : I suppressed the ":" here, since 
+       ;; "Definition foo [x:bar]..." is allowed
        ((and (not (coq-goal-command-p str))
 	     (proof-string-match
-	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str))
+	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str))
 	(setq ans (format coq-forget-id-command (match-string 2 str)))))
 
       (setq span (next-span span 'type)))
-- 
cgit v1.2.3