From 471b212179ddec4c0e49b2cbc4d1750f6738a623 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sat, 21 Jan 2017 18:19:02 +0100
Subject: [PATCH] Make it possible to apply the observational view shift
 lemmas.

---
 theories/program_logic/adequacy.v | 4 ++--
 theories/program_logic/ownp.v     | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 2c9ce1d1e..6f442eb45 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -187,11 +187,11 @@ Proof.
     iFrame. by iApply big_sepL_nil.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ},
      True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e {{ Φ }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
+       stateI σ1 ∗ WP e {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
   rtc step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 6d318ea72..54fb03310 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -50,13 +50,13 @@ Proof.
   iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
 
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ :
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
   (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e {{ Φ }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+    ownP σ1 ={⊤}=∗ WP e {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _ Φ)=> //.
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _)=> //.
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
     as (γσ) "[Hσ Hσf]"; first done.
   iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
-- 
GitLab