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).

1 files 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                               ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;