diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index b9cdfe06310e65f9cd73c01d4f51a402df979ffa..fb4a555d87cc409306c4475e98ccf137fcaffde2 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 0af5b474d9af1e5030f0e4df52c3a87c0e161e95..846b4956589900e43c41cdeebe18e6770b69a642 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 8ef2706a39305457371b66a9e76350ea2a33cd23..43755f2c6a48b47a98d2f32309fdf00f4bb135fb 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.