diff --git a/theories/typing/type.v b/theories/typing/type.v
index 0e2ed5ec73e730927a53887160bb31a5d2ae998c..a97757f1a3b3344f9154229ad251be5c6419dc77 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -169,8 +169,8 @@ Section ofe.
   Instance type_dist : Dist type := type_dist'.
 
   Let T := prodO
-    (prodO natO (thread_id -d> list val -d> vPropC Σ))
-    (lft -d> thread_id -d> loc -d> vPropC Σ).
+    (prodO natO (thread_id -d> list val -d> vPropO Σ))
+    (lft -d> thread_id -d> loc -d> vPropO Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
@@ -234,7 +234,7 @@ Section ofe.
       st_dist' n ty1 ty2.
   Instance st_dist : Dist simple_type := st_dist'.
 
-  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> vPropC Σ :=
+  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> vPropO Σ :=
     λ tid vl, ty.(ty_own) tid vl.
 
   Definition st_ofe_mixin : OfeMixin simple_type.