From 56301ac8990034b819eb97993288de133a84fa28 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Oct 2016 09:10:44 +0200
Subject: [PATCH] Also create a wand when reverting a persistent hypothesis.

This is more consistent with our current consensus of not using
implication. Also, it allows one to reintroduce the persistent
hypothesis into the spatial context.
---
 proofmode/coq_tactics.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index d520cf9a8..314356e66 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -578,11 +578,10 @@ Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
-  (Δ' ⊢ if p then □ P → Q else P -★ Q) → Δ ⊢ Q.
+  (Δ' ⊢ (if p then □ P else P) -★ Q) → Δ ⊢ Q.
 Proof.
-  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
-  - by rewrite HQ -always_and_sep_l impl_elim_r.
-  - by rewrite HQ wand_elim_r.
+  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
+  by rewrite HQ /uPred_always_if wand_elim_r.
 Qed.
 
 Lemma tac_revert_ih Δ P Q :
-- 
GitLab