From fda5c51c16ac7947dff5165264e2b5f28895f23f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Mar 2017 09:59:04 +0100
Subject: [PATCH] proof tuning

---
 theories/program_logic/ectx_lifting.v | 2 +-
 theories/program_logic/lifting.v      | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index bac5de8a2..64a1ce2dc 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -38,7 +38,7 @@ Lemma wp_lift_pure_head_step {E E' Φ} e1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
-  iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
+  iMod "H". iModIntro. iNext. iMod "H". iModIntro.
   iIntros (????). iApply "H". eauto.
 Qed.
 
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 2aebb9a24..0b6c2dc41 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -30,11 +30,11 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { eapply reducible_not_val, (Hsafe inhabitant). }
-  iIntros (σ1) "Hσ". iMod "H" as "H".
+  iIntros (σ1) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
   iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
-  iMod "Hclose" as "_". iFrame "Hσ". iMod "H" as "H". iApply "H"; auto.
+  iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
@@ -66,7 +66,7 @@ Proof.
   iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
   { by intros; eapply Hpuredet. }
   (* TODO: Can we make this nicer? iNext for fupd, for example, could help. *)
-  iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
+  iMod "H". iModIntro. iNext. iMod "H". iModIntro.
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.
-- 
GitLab