From 0fcb5b61f8f8816fb83d63b4b2118ed2c3a8af8b Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sat, 5 Oct 2019 11:20:42 +0200
Subject: [PATCH] fix missing renaming vPropC to vPropO

---
 theories/typing/type.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 0e2ed5ec..a97757f1 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.
-- 
GitLab