branch: elpa/proof-general
commit 3a2af43ce973ac4a6dce336181a04914a67d2d4a
Merge: 809b01e845 28497cd899
Author: Pierre Courtieu <mata...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #813 from Matafou/fix-real-start
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 7ceff93281..aab99837fa 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -217,10 +217,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 2b83a1ddd4..b57220a9af 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2504,13 +2504,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) ")."))
@@ -2711,6 +2713,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))
