branch: elpa/proof-general
commit 74ba7fc6de735e9d8f262dd6a3c580db9ea9b077
Merge: 1024beb7a1f b82c21961f2
Author: Pierre Courtieu <[email protected]>
Commit: Pierre Courtieu <[email protected]>
Merge branch 'master' into fix-elpi-parsing
---
ci/test-indent/indent-tac-boxed.v | 22 ++++++++++++++++++++++
ci/test-indent/indent-tac.v | 22 ++++++++++++++++++++++
coq/coq-smie.el | 2 +-
3 files changed, 45 insertions(+), 1 deletion(-)
diff --git a/ci/test-indent/indent-tac-boxed.v
b/ci/test-indent/indent-tac-boxed.v
index 8c37d910ea2..84c7de89c04 100644
--- a/ci/test-indent/indent-tac-boxed.v
+++ b/ci/test-indent/indent-tac-boxed.v
@@ -153,6 +153,28 @@ Module curlybracesatend.
simpl.
rewrite Nat.add_1_r.
reflexivity.
+ intros r. {
+ now exists
+ {|
+ fld1:=r.(fld2);
+ fld2:=r.(fld1);
+ fld3:=false
+ |}.
+ split.
+ {auto. }
+ {auto. }
+ }
+ intros r. {
+ try exists
+ {|
+ fld1:=r.(fld2);
+ fld2:=r.(fld1);
+ fld3:=false
+ |}.
+ split.
+ {auto. }
+ {auto. }
+ }
}
}
idtac.
diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
index 77a9987685b..ff443476468 100644
--- a/ci/test-indent/indent-tac.v
+++ b/ci/test-indent/indent-tac.v
@@ -417,6 +417,28 @@ Module X.
{auto. }
{auto. }
}
+ intros r. {
+ now exists
+ {|
+ fld1:=r.(fld2);
+ fld2:=r.(fld1);
+ fld3:=false
+ |}.
+ split.
+ {auto. }
+ {auto. }
+ }
+ intros r. {
+ split.
+ - now exists x.
+ split.
+ {auto. }
+ {auto. }
+ - now exists x.
+ split.
+ {auto. }
+ {auto. }
+ }
intros r. {
exists
{|
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 5528c65586a..719b3d3aeb3 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -835,7 +835,7 @@ The point should be at the beginning of the command name."
(let ((prevtok (coq-smie-backward-token)))
;; => may be wrong here but rare (have "=> ltac"?)
(not (or (coq-is-cmdend-token prevtok)
- (member prevtok '("; tactic" "[" "]" "|" "=>")))))))
+ (member prevtok '("; tactic" "[" "]" "|" "=>" "Com
start")))))))
"quantif exists")
((equal tok "∀") "forall")
