From 672dff6dfcafa723f6a781c679ad3548e101ef2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 May 2016 18:42:10 +0200
Subject: [PATCH] Use proper notations in saved_prop.

---
 program_logic/saved_one_shot.v | 16 +++++++---------
 program_logic/saved_prop.v     |  6 +++---
 2 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/program_logic/saved_one_shot.v b/program_logic/saved_one_shot.v
index 846b49565..c8a9a27f0 100644
--- a/program_logic/saved_one_shot.v
+++ b/program_logic/saved_one_shot.v
@@ -25,26 +25,24 @@ Section one_shot.
   Global Instance ne_shot_own_persistent γ x : PersistentP (one_shot_own γ x).
   Proof. rewrite /one_shot_own; apply _. Qed.
 
-  Lemma one_shot_alloc_strong N (G : gset gname) :
-    True ⊢ pvs N N (∃ γ, ■ (γ ∉ G) ∧ one_shot_pending γ).
+  Lemma one_shot_alloc_strong E (G : gset gname) :
+    True ⊢ |={E}=> ∃ γ, ■ (γ ∉ G) ∧ one_shot_pending γ.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma one_shot_alloc N : True ⊢ pvs N N (∃ γ, one_shot_pending γ).
+  Lemma one_shot_alloc E : True ⊢ |={E}=> ∃ γ, one_shot_pending γ.
   Proof. by apply own_alloc. Qed.
 
-  Lemma one_shot_init N γ x :
-    one_shot_pending γ ⊢ pvs N N (one_shot_own γ x).
+  Lemma one_shot_init E γ x : one_shot_pending γ ⊢ |={E}=> one_shot_own γ x.
   Proof. by apply own_update, one_shot_update_shoot. Qed.
 
-  Lemma one_shot_alloc_init N x : True ⊢ pvs N N (∃ γ, one_shot_own γ x).
+  Lemma one_shot_alloc_init E x : True ⊢ |={E}=> ∃ γ, one_shot_own γ x.
   Proof.
-    rewrite (one_shot_alloc N). apply pvs_strip_pvs.
+    rewrite (one_shot_alloc E). apply pvs_strip_pvs.
     apply exist_elim=>γ. rewrite -(exist_intro γ).
     apply one_shot_init.
   Qed.
 
-  Lemma one_shot_agree γ x y :
-    (one_shot_own γ x ★ one_shot_own γ y) ⊢ ▷(x ≡ y).
+  Lemma one_shot_agree γ x y : (one_shot_own γ x ★ one_shot_own γ y) ⊢ ▷(x ≡ y).
   Proof.
     rewrite -own_op own_valid one_shot_validI /= agree_validI.
     rewrite agree_equivI later_equivI.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 43755f2c6..2a4016cb3 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -23,11 +23,11 @@ Section saved_prop.
   Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
-  Lemma saved_prop_alloc_strong N x (G : gset gname) :
-    True ⊢ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x).
+  Lemma saved_prop_alloc_strong E x (G : gset gname) :
+    True ⊢ |={E}=> ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc N x : True ⊢ pvs N N (∃ γ, saved_prop_own γ x).
+  Lemma saved_prop_alloc E x : True ⊢ |={E}=> ∃ γ, saved_prop_own γ x.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ x y :
-- 
GitLab