Fix name clash & rephrase some strings

coq/coq-abbrev.el

@@ -259,11 +259,11 @@
        :style radio
        :selected (eq coq-diffs 'removed)
        :help "Show diffs: added and removed"])
-    ["Show proof diffs"
-      coq-show-proof-toggle
+    ["Show Proof (Diffs)"
+      coq-show-proof-stepwise-toggle
       :style toggle
-      :selected coq-show-proof
-      :help "Show the proof diffs in the response buffer"]
+      :selected coq-show-proof-stepwise
+      :help "Display the proof terms stepwise in the *response* buffer."]
     ("\"Proof using\" mode..."
      ["ask"
       (customize-set-variable 'coq-accept-proof-using-suggestion 'ask)

coq/coq-compile-common.el

@@ -459,14 +459,14 @@ This option can be set via menu
 (proof-deftoggle coq-lock-ancestors)
 
 ;; Maybe not the good place
-(defcustom coq-show-proof nil
+(defcustom coq-show-proof-stepwise nil
   "TODO: doc"
 
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
 
-(proof-deftoggle coq-show-proof)
+(proof-deftoggle coq-show-proof-stepwise)
 
 (defcustom coq-confirm-external-compilation t
   "If set let user change and confirm the compilation command.

coq/coq-showdiff.el

@@ -2,11 +2,11 @@
 (defun coq-show-proof-fun ()
   (interactive)
   ;; TODO: Check if we are in a proof
-  (when coq-show-proof
+  (when coq-show-proof-stepwise
     (when (eq coq-diffs 'off)
       (proof-shell-invisible-command "Show Proof." ))
     (when (eq coq-diffs 'on)
       (proof-shell-invisible-command "Show Proof Diffs."))
     (when (eq coq-diffs 'removed)
       (proof-shell-invisible-command "Show Proof Diffs removed.")))
- )
+ )

coq/coq-syntax.el

@@ -1304,7 +1304,8 @@ It is used:
   "*Font-lock table for Coq terms.")
 
 
-(defconst coq-show-diffs-regexp
+(defconst coq-show-proof-diffs-regexp
+  ;; FIXME/TODO: enhance this regexp
   "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)")
 
 (defconst coq-save-command-regexp

coq/coq.el

@@ -1208,7 +1208,7 @@ be called and no command will be sent to Coq."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
-    (if coq-show-proof
+    (if coq-show-proof-stepwise
         (or
     (when (eq coq-diffs 'off) (list "Show." "Show Proof." ))
     (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs."))
@@ -1221,7 +1221,7 @@ 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)
-                            (if coq-show-proof
+                            (if coq-show-proof-stepwise
     ((when (eq coq-diffs 'off)
       "Show." "Show Proof." )
     (when (eq coq-diffs 'on)
@@ -1240,7 +1240,7 @@ 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
+          (when coq-show-proof-stepwise
             (list "Show." "Show Proof.")))))))
 
 
@@ -1910,7 +1910,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
         proof-save-command "Save %s. "
         proof-find-theorems-command "Search %s. ")
 
-  (setq proof-show-diffs-regexp coq-show-diffs-regexp)
+  (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp)
 
   (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command)
 

generic/proof-config.el

@@ -399,7 +399,7 @@ NB: This setting is not used for matching output from the prover."
   :type 'regexp
   :group 'proof-script)
 
-(defcustom proof-show-diffs-regexp nil
+(defcustom proof-show-proof-diffs-regexp nil
   "Matches all Show Proof form"
   :type 'regexp
   :group 'proof-script)