From 2bea47fca9a2a4d1303d2a915cd0f8c3ec4ec206 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:29:23 +0200
Subject: [PATCH] `iRevert` of a pure hypotheses generates a wand instead of
 implication.

---
 iris/proofmode/coq_tactics.v  | 10 ++++++++--
 iris/proofmode/ltac_tactics.v |  5 ++++-
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index a2708b041..060f818cd 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -170,8 +170,14 @@ Proof.
       rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
-Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
-Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
+Lemma tac_pure_revert Δ φ P Q :
+  FromAffinely P ⌜ φ ⌝ →
+  envs_entails Δ (P -∗ Q) →
+  (φ → envs_entails Δ Q).
+Proof.
+  rewrite /FromAffinely envs_entails_eq. intros <- -> ?.
+  by rewrite pure_True // affinely_True_emp affinely_emp left_id.
+Qed.
 
 (** * Intuitionistic *)
 Lemma tac_intuitionistic Δ i j p P P' Q :
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index f4da0ed78..b651b3fbf 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -651,7 +651,10 @@ Local Tactic Notation "iForallRevert" ident(x) :=
   first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
   let A := type of x in
   lazymatch type of A with
-  | Prop => revert x; first [apply tac_pure_revert|err x]
+  | Prop =>
+     revert x; first
+       [eapply tac_pure_revert; [iSolveTC (* [FromAffinely], should never fail *)|]
+       |err x]
   | _ => revert x; first [apply tac_forall_revert|err x]
   end.
 
-- 
GitLab