diff options
author | 2000-11-24 14:26:50 +0000 | |
---|---|---|
committer | 2000-11-24 14:26:50 +0000 | |
commit | 20f205b75f0de1de10d31196256d143c8031447c (patch) | |
tree | b3edfda9af40c04889234aea4125b2743b4b0322 /coq | |
parent | 22b791f0c77d8063153939cd02295c01b2d20cc4 (diff) |
Add a little change to coq-find-and-forget to work better
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -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))) |