From f90caf7fdcbeef648342f86966f12ea0076888c8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 12:25:01 +0200
Subject: [PATCH] Make sure that `iRevert` preserves names and does not invent
fresh ones.
---
iris/proofmode/ltac_tactics.v | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 42e4e4c31..958f3a164 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -637,9 +637,18 @@ Local Tactic Notation "iForallRevert" ident(x) :=
lazymatch type of A with
| Prop =>
revert x; first
- [eapply tac_pure_revert; [tc_solve (* [FromAffinely], should never fail *)|]
+ [eapply tac_pure_revert;
+ [tc_solve (* [FromAffinely], should never fail *)
+ |]
|err x]
- | _ => revert x; first [apply tac_forall_revert|err x]
+ | _ =>
+ revert x; first
+ [apply tac_forall_revert;
+ lazymatch goal with
+ | |- envs_entails ?Δ (∀ y, @?P y) =>
+ change (envs_entails Δ (∀ x, P x)); lazy beta
+ end
+ |err x]
end.
(** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
--
GitLab