From b0ed77483e1e331fbd8a570bdf3a1281f7484b9c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 May 2016 13:34:36 +0200
Subject: [PATCH] Add notation iPrePropG.

---
 program_logic/global_functor.v | 3 ++-
 program_logic/saved_one_shot.v | 2 +-
 program_logic/saved_prop.v     | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index b9cdfe063..fb4a555d8 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -20,6 +20,7 @@ Definition gname := positive.
 Definition globalF (Σ : gFunctors) : iFunctor :=
   IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))).
 Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
+Notation iPrePropG Λ Σ := (iPreProp Λ (globalF Σ)).
 
 Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
   inG_id : gid Σ;
@@ -114,7 +115,7 @@ their first argument to avoid loops. For example, the instances [authGF_inGF]
 and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
 Hint Mode inGF + + - : typeclass_instances.
 
-Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPreProp Λ (globalF Σ))).
+Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPrePropG Λ Σ)).
 Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
 Instance inGF_here {Λ Σ} (F: gFunctor) : inGF Λ (gFunctors.cons F Σ) F.
 Proof. by exists 0%fin. Qed.
diff --git a/program_logic/saved_one_shot.v b/program_logic/saved_one_shot.v
index 0af5b474d..846b49565 100644
--- a/program_logic/saved_one_shot.v
+++ b/program_logic/saved_one_shot.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership.
 Import uPred.
 
 Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
-  one_shot_inG :> inG Λ Σ (one_shotR $ agreeR $ laterC $ F (iPreProp Λ (globalF Σ))).
+  one_shot_inG :> inG Λ Σ (one_shotR $ agreeR $ laterC $ F (iPrePropG Λ Σ)).
 Definition oneShotGF (F : cFunctor) : gFunctor :=
   GFunctor (one_shotRF (agreeRF (â–¶ F))).
 Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 8ef2706a3..43755f2c6 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership.
 Import uPred.
 
 Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
-  saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))).
+  saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPrePropG Λ Σ)))).
 Definition savedPropGF (F : cFunctor) : gFunctor :=
   GFunctor (agreeRF (â–¶ F)).
 Instance inGF_savedPropG  `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
-- 
GitLab