From 05a120275c557e95c73c7c2bdd1e2725197d3bd0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 30 Jan 2003 20:08:19 +0000
Subject: Bug correction in the find-and-forget function for coq: in Coq v74,
 no prompt is return if an empty command is send ("\n"), so if the command is
 empty, we send proof-no-command (if not, backtracking state preserving
 command stays indefinitely in "proof process busy" state).

---
 coq/coq.el | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index f0daec25..5f1b9d03 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -378,9 +378,12 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
            (if (> nundos 0) 
                (concat "Undo " (int-to-string nundos) ". "))))
 
-    (if (null ans) 
-        proof-no-command;; FIXME: this is an error really (assert nil)
-      ans)))
+    (if (null ans) proof-no-command;; FIXME: this is an error really (assert nil); 
+      (if (string-equal ans "") proof-no-command ; not here because if
+						 ; we backtrack a state preserving command, we must do
+						 ; *nothing*, not even a CR (in v74, no prompt is returned
+						 ; with "\n")
+      ans))))
   
 
 (defvar coq-current-goal 1
@@ -571,6 +574,7 @@ This is specific to coq-mode."
 	   " -emacs"))
       coq-prog-name)))
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Coq shell startup and exit hooks                               ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3