From a18b8e18db2cfc1e38589c0c7a67709538cf77be Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 1 Mar 2021 12:03:11 +0100
Subject: [PATCH] avoid relying on rewrite's implicit revert

---
 iris/proofmode/coq_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 3be114662..0451e6559 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -539,7 +539,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
 Proof.
   destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
   destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
-  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
+  rewrite envs_entails_eq. move: Hlookup. rewrite envs_lookup_delete_Some.
   intros [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
-- 
GitLab