From 4b2801a521f7365f8a3833fa9805828792dac853 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 28 Sep 2009 08:40:57 +0000
Subject: Functions find-and-forget and count-undos now return lists of
 commands

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 2543eedd..8921ca82 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -306,7 +306,7 @@ used see coq-set-state-number. Initially 1 because Coq initial state has number
 (defun coq-set-state-infos ()
   "Set the last locked span's state number to the number found last time.
 This number is in the *last but one* prompt (variable `coq-last-but-one-statenum').
-If locked span already has a state number, thne do nothing. Also updates
+If locked span already has a state number, then do nothing. Also updates
 `coq-last-but-one-statenum' to the last state number for next time."
   (if (and proof-shell-last-prompt proof-script-buffer)
       ;; infos = promt infos of the very last prompt
@@ -387,10 +387,11 @@ If locked span already has a state number, thne do nothing. Also updates
              (equal coq-last-but-one-proofstack proofstack)
              (= coq-last-but-one-proofnum proofdepth)
              (= coq-last-but-one-statenum span-staten))
-      (format "Backtrack %s %s %s . "
-              (int-to-string span-staten)
-              (int-to-string proofdepth)
-              naborts))))
+      (list
+       (format "Backtrack %s %s %s . "
+               (int-to-string span-staten)
+               (int-to-string proofdepth)
+               naborts)))))
 
 (defvar coq-current-goal 1
   "Last goal that Emacs looked at.")
-- 
cgit v1.2.3