From c8373c01a54f0e0ee7fafbf080e98003f8179aec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 12:27:51 +0200
Subject: [PATCH] Comment.
---
iris/proofmode/ltac_tactics.v | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 958f3a164..8efc6955b 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -644,6 +644,7 @@ Local Tactic Notation "iForallRevert" ident(x) :=
| _ =>
revert x; first
[apply tac_forall_revert;
+ (* Ensure the name [x] is preserved, see [test_iRevert_order_and_names]. *)
lazymatch goal with
| |- envs_entails ?Δ (∀ y, @?P y) =>
change (envs_entails Δ (∀ x, P x)); lazy beta
@@ -676,7 +677,10 @@ Tactic Notation "iRevert" constr(Hs) :=
go Hs
| ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
end in
- iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
+ iStartProof;
+ let Hs := iElaborateSelPat Hs in
+ (* No need to reverse [Hs], [iElaborateSelPat] already does that. *)
+ go Hs.
Tactic Notation "iRevert" "(" ident(x1) ")" :=
iForallRevert x1.
--
GitLab