[nongnu] elpa/proof-general 28497cd899 05/10: Fix low level code to find the start of a command.

[ELPA Syncer]

branch: elpa/proof-general
commit 28497cd899d11948ceff601929d062f8a92524df
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    Fix low level code to find the start of a command.
---
 ci/test-indent/indent-tac.v | 13 +++++++++++++
 coq/coq-indent.el           |  4 ++--
 coq/coq.el                  |  5 ++++-
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
index 4a27e7038b..77a9987685 100644
--- a/ci/test-indent/indent-tac.v
+++ b/ci/test-indent/indent-tac.v
@@ -269,6 +269,19 @@ Module M1.
         { auto.
         }
       }
+      1:{
+        destruct n.
+        2:{ auto.
+        }
+        { auto. }
+      }
+      {
+        destruct n.
+        2:{
+          auto. }
+        { auto.
+        }
+      }
     Qed.
   End M2.
 End M1.
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index b1e3e0425b..cc066e694e 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -216,10 +216,10 @@ position."
     (coq-find-previous-endcmd)
     (while (not something-found)
       (forward-comment (point-max))
-      (if (and (looking-at "\\({\\|}\\|\\++\\|\\*+\\|-+\\)")
+      (if (and (looking-at "\\(?1:{\\|}\\|\\++\\|\\*+\\|-+\\|[0-9]+\\s-*:{\\)")
                (< (point) p) ;; if we are after the starting point then 
anything is the start of the current command, even "#" or ".".
                )
-          (forward-char 1)
+          (goto-char (match-end 1))
         (setq something-found t))))
   (point))
 
diff --git a/coq/coq.el b/coq/coq.el
index 4eb4938106..130a948e68 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2500,13 +2500,15 @@ tacitcs like destruct and induction reuse hypothesis 
names by
 default, which makes the detection of new hypothesis incorrect.
 the hack consists in adding the \"!\" modifier on the argument
 destructed, so that it is left in the goal and the name cannot be
-reused.  We also had a \"clear\" at the end of the tactic so that
+reused.  We also add a \"clear\" at the end of the tactic so that
 the whole tactic behaves correctly.
 Warning: this makes the error messages (and location) wrong.")
 
 (defun coq-hack-cmd-for-infoH (s)
   "return the tactic S hacked with infoH tactical."
   (cond
+   ;; We cannot rebuild the sub-patterns from the final goal, so ';' is not
+   ;; supported. Only single tactics like destruct.
    ((string-match ";" s) s) ;; composed tactic cannot be treated
    ((string-match coq-auto-as-hack-hyp-name-regex s)
     (concat "infoH " (match-string 1 s) " (" (match-string 2 s) ")."))
@@ -2707,6 +2709,7 @@ Used for automatic insertion of \"Proof using\" 
annotations.")
   (interactive)
   (save-excursion
     (goto-char (proof-unprocessed-begin))
+    (forward-char 1)
     (coq-find-real-start)
     (let* ((pt (point))
            (_ (coq-script-parse-cmdend-forward))