From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Mon, 25 May 2020 10:55:03 +0200
Subject: fix: backtrack wrong type argument

---
 coq/coq-syntax.el |  2 +-
 coq/coq.el        | 40 +++++++++++++++++++++-------------------
 2 files changed, 22 insertions(+), 20 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 47869aed..5b8d8c48 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1305,7 +1305,7 @@ It is used:
 
 
 (defconst coq-show-proof-diffs-regexp
-  "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b")
+  "\\`Show Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\'")
 
 (defconst coq-save-command-regexp
   ;; FIXME: The surrounding grouping parens are probably not needed.
diff --git a/coq/coq.el b/coq/coq.el
index 10aa07bf..9fc6e200 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -162,9 +162,9 @@ See also option `coq-hide-additional-subgoals'."
 
 (defcustom coq-show-proof-stepwise nil
   "Display the proof terms stepwise in the *response* buffer.
-  This option can be combined with option `coq-diffs'.
-  It is mostly useful in three window mode, see also
-  `proof-three-window-mode-policy' for details."
+This option can be combined with option `coq-diffs'.
+It is mostly useful in three window mode, see also
+`proof-three-window-mode-policy' for details."
 
   :type 'boolean
   :safe 'booleanp
@@ -1209,7 +1209,9 @@ Printing All set."
   "Return the list of commands to send to Coq after CMD
 if it is the last command of the action list.
 If CMD is tagged with 'empty-action-list then this function won't
-be called and no command will be sent to Coq."
+be called and no command will be sent to Coq.
+Note: the last command added if `coq-show-proof-stepwise' is set
+should match the `coq-show-proof-diffs-regexp'."
   (cond
    ((or
      ;; If closing a nested proof, Show the enclosing goal.
@@ -1219,11 +1221,11 @@ be called and no command will be sent to Coq."
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
     (list "Show."
-    (when coq-show-proof-stepwise
-        (or
-    (when (eq coq-diffs 'off) "Show Proof.")
-    (when (eq coq-diffs 'on) "Show Proof Diffs.")
-    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+          (when coq-show-proof-stepwise
+            (or
+             (when (eq coq-diffs 'off) "Show Proof.")
+             (when (eq coq-diffs 'on) "Show Proof Diffs.")
+             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
    
    ((or
      ;; If we go back in the buffer and the number of abort is less than
@@ -1232,11 +1234,11 @@ be called and no command will be sent to Coq."
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
     (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
-                                  (when coq-show-proof-stepwise
-                                    (or
-    (when (eq coq-diffs 'off) "Show Proof.")
-    (when (eq coq-diffs 'on) "Show Proof Diffs.")
-    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+          (when coq-show-proof-stepwise
+            (or
+             (when (eq coq-diffs 'off) "Show Proof.")
+             (when (eq coq-diffs 'on) "Show Proof Diffs.")
+             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
 
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
@@ -1251,11 +1253,11 @@ be called and no command will be sent to Coq."
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)))
-          (when coq-show-proof-stepwise
-              (or
-    (when (eq coq-diffs 'off) (list "Show Proof." ))
-    (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
+    (when coq-show-proof-stepwise
+      (or
+       (when (eq coq-diffs 'off) (list "Show Proof." ))
+       (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
+       (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
 
 
 (defpacustom auto-adapt-printing-width t
-- 
cgit v1.2.3