From d2cbc541b27673cfe9a5f08142174e5701862c51 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Jun 2019 21:46:39 +0200
Subject: [PATCH] =?UTF-8?q?Bump=20Iris=20(C=E2=86=92O=20rename).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 opam                                  |  2 +-
 theories/lang/arc.v                   |  2 +-
 theories/lang/arc_cmra.v              |  4 ++--
 theories/lang/lock.v                  |  2 +-
 theories/lang/spawn.v                 |  4 ++--
 theories/lifetime/lifetime.v          |  2 +-
 theories/lifetime/model/boxes.v       | 14 +++++++-------
 theories/lifetime/model/definitions.v | 10 +++++-----
 theories/typing/lib/rc/rc.v           |  2 +-
 theories/typing/lib/refcell/refcell.v |  2 +-
 theories/typing/lib/rwlock/rwlock.v   |  2 +-
 theories/typing/type.v                | 14 +++++++-------
 12 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/opam b/opam
index 13acad72..1d2b94b9 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-05-29.0.c71ac064") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-06-18.0.f72f5a19") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 2a5e332b..2c3042fc 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1900,7 +1900,7 @@ Section arc.
       iSplitR "HP2 SW SM SD oW SDA tok"; [|iSplitL""]; [..|by iFrame]; last first.
       { iIntros (t2 [] [_ Ext2]). iSplit.
         - iIntros "!> (_&_&_&_&_&SDA&_)".
-          iDestruct 1 as "[Eq NC]". iDestruct "NC" as (t3 Lt3) "Cert".
+          iDestruct 1 as "[Eq NO]". iDestruct "NO" as (t3 Lt3) "Cert".
           iDestruct (StrongDownAuth_Cert_include with "[$SDA $Cert]")
             as %Le3%elem_of_subseteq_singleton%MAX. exfalso.
           apply (irreflexive_eq (R:=Pos.lt) t1 t1); [done|].
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 6d6871a6..71210a3a 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -25,7 +25,7 @@ Set Default Proof Using "Type".
   i.e. the caller being unique. A persistent certificate is issued when the
   authority is updated. A fraction of the authority must have seen all certificates. *)
 Definition move_selfUR :=
-  prodUR (authUR (optionUR (prodR fracR (agreeR (latC (gset_Lat time))))))
+  prodUR (authUR (optionUR (prodR fracR (agreeR (latO (gset_Lat time))))))
         (authUR (latUR (gset_Lat time))).
 
 (* This cmra tracks what the arc has asked the other to do, e.g., the weak arc
@@ -54,7 +54,7 @@ Definition move_otherUR :=
 
 Definition weak_stUR :=
   prodUR (optionUR fracR)
-         (optionUR (csumR (prodR fracR positiveR) (prodR (exclR unitC) (agreeR fracC)))).
+         (optionUR (csumR (prodR fracR positiveR) (prodR (exclR unitO) (agreeR fracO)))).
 
 (* This cmra tracks states of the strong counter:
   - None: no strong arc, v = 0.
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index a1f94977..46f48b90 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -21,7 +21,7 @@ Class lockG Σ := LockG {
 }.
 
 Definition lockΣ : gFunctors :=
-  #[gpsΣ unitProtocol; GFunctor (agreeR (leibnizC time))].
+  #[gpsΣ unitProtocol; GFunctor (agreeR (leibnizO time))].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index ff702ed1..03595309 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -30,11 +30,11 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 Class spawnG Σ := SpawnG {
-  spawn_tokG :> inG Σ (exclR unitC);
+  spawn_tokG :> inG Σ (exclR unitO);
   spawn_gpsG :> gpsG Σ unitProtocol;
   spawn_viewG :> view_invG Σ }.
 
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC); gpsΣ unitProtocol; view_invΣ].
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO); gpsΣ unitProtocol; view_invΣ].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 283b2572..880b4c42 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -23,7 +23,7 @@ Notation lft_intersect_list l := (foldr lft_intersect static l).
 
 Instance lft_inhabited : Inhabited lft := populate static.
 
-Canonical lftC := leibnizC lft.
+Canonical lftO := leibnizO lft.
 
 Section derived.
 Context `{!invG Σ, !lftG Lat E0 Σ}.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 2c2741cc..3091f461 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -11,12 +11,12 @@ Implicit Types Lat : latticeT.
 (** The CMRAs we need. *)
 Class boxG Lat Σ :=
   boxG_inG :> inG Σ (prodR
-    (authR (optionUR (exclR (optionC (latC Lat)))))
-    (optionR (agreeR (laterC (Lat -c> iPreProp Σ))))).
+    (authR (optionUR (exclR (optionO (latO Lat)))))
+    (optionR (agreeR (laterO (Lat -d> iPreProp Σ))))).
 
 Definition boxΣ Lat : gFunctors := #[
-   GFunctor (authR (optionUR (exclR (optionC (latC Lat)))) *
-   optionRF (agreeRF (▶ (Lat -c> ∙))) ) ].
+   GFunctor (authR (optionUR (exclR (optionO (latO Lat)))) *
+   optionRF (agreeRF (▶ (Lat -d> ∙))) ) ].
 
 Instance subG_stsΣ Lat Σ : subG (boxΣ Lat) Σ → boxG Lat Σ.
 Proof. solve_inG. Qed.
@@ -32,7 +32,7 @@ Section box_defs.
     own γ (a, ε).
 
   Definition box_own_prop (γ : slice_name) (P : monPred) : iProp :=
-    own γ (ε, Some (to_agree (Next (iProp_unfold ∘ P : _ -c> _)))).
+    own γ (ε, Some (to_agree (Next (iProp_unfold ∘ P : _ -d> _)))).
 
   Definition slice_inv (γ : slice_name) (P : monPred) : iProp :=
     (∃ o, box_own_auth γ (● Excl' o) ∗ from_option (P ∘ of_latT) True o)%I.
@@ -111,7 +111,7 @@ Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
   rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
   iIntros "#HQ". iApply monPred_equivI. iIntros (V).
-  iApply iProp_unfold_equivI. rewrite ofe_fun_equivI. iNext. iApply "HQ".
+  iApply iProp_unfold_equivI. rewrite discrete_fun_equivI. iNext. iApply "HQ".
 Qed.
 
 Lemma box_alloc : box N ∅ True%I.
@@ -125,7 +125,7 @@ Lemma slice_insert_empty E q f Q P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' None ⋅ ◯ Excl' None,
-    Some (to_agree (Next ((λ V, iProp_unfold (Q V)) : _ -c> _)))) (dom _ f))
+    Some (to_agree (Next ((λ V, iProp_unfold (Q V)) : _ -d> _)))) (dom _ f))
     as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid|done]. }
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 9dde6009..15479065 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -27,19 +27,19 @@ Inductive bor_state {Lat} :=
   | Bor_rebor (κ : lft) (V : Lat).
 Arguments bor_state : clear implicits.
 
-Canonical Structure bor_stateC Lat := leibnizC (bor_state Lat).
+Canonical Structure bor_stateO Lat := leibnizO (bor_state Lat).
 
 Record lft_names := LftNames {
   bor_name : gname;
   cnt_name : gname;
   inh_name : gname
 }.
-Canonical lft_namesC := leibnizC lft_names.
+Canonical lft_namesO := leibnizO lft_names.
 
-Definition lft_stateR Lat := csumR (prodR fracR (latR Lat)) (agreeR (latC Lat)).
+Definition lft_stateR Lat := csumR (prodR fracR (latR Lat)) (agreeR (latO Lat)).
 Definition alftUR Lat := gmapUR atomic_lft (lft_stateR Lat).
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
-Definition borUR Lat := gmapUR slice_name (exclR (bor_stateC Lat)).
+Definition ilftUR := gmapUR lft (agreeR lft_namesO).
+Definition borUR Lat := gmapUR slice_name (exclR (bor_stateO Lat)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftG Lat E0 Σ := LftG {
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 8401a501..a64d605a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -7,7 +7,7 @@ From lrust.typing Require Import typing option.
 Set Default Proof Using "Type".
 
 Definition rc_stR :=
-  prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
+  prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
   RcG :> inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 43924772..45cb8549 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 Definition refcell_stR :=
   optionUR (prodR (prodR
-             (agreeR (prodC lftC boolC))
+             (agreeR (prodO lftO boolO))
              fracR)
              positiveR).
 Class refcellG Σ :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index ad4b117e..4305c315 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
 Definition rwlock_st := option (() + lft * frac * positive).
 
 Definition rwlock_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
+  optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Definition rwlockR := authR rwlock_stR.
 Class rwlockG Σ := RwLockG {
   rwlock_stateG :> inG Σ rwlockR ;
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 4e054112..7672f3cf 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -168,9 +168,9 @@ Section ofe.
       type_dist' n ty1 ty2.
   Instance type_dist : Dist type := type_dist'.
 
-  Let T := prodC
-    (prodC natC (thread_id -c> list val -c> vPropC Σ))
-    (lft -c> thread_id -c> loc -c> vPropC Σ).
+  Let T := prodO
+    (prodO natO (thread_id -d> list val -d> vPropC Σ))
+    (lft -d> thread_id -d> loc -d> vPropC Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
@@ -191,7 +191,7 @@ Section ofe.
     - split; [by destruct 1|by intros [[??] ?]; constructor].
     - split; [by destruct 1|by intros [[??] ?]; constructor].
   Qed.
-  Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
+  Canonical Structure typeO : ofeT := OfeT type type_ofe_mixin.
 
   Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
   Proof. intros ?? EQ. apply EQ. Qed.
@@ -209,7 +209,7 @@ Section ofe.
     Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
   Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
 
-  Global Instance type_cofe : Cofe typeC.
+  Global Instance type_cofe : Cofe typeO.
   Proof.
     apply (iso_cofe_subtype' P type_pack type_unpack).
     - by intros [].
@@ -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 -c> list val -c> vPropC Σ :=
+  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> vPropC Σ :=
     λ tid vl, ty.(ty_own) tid vl.
 
   Definition st_ofe_mixin : OfeMixin simple_type.
@@ -243,7 +243,7 @@ Section ofe.
     - split; [by destruct 1|by constructor].
     - split; [by destruct 1|by constructor].
   Qed.
-  Canonical Structure stC : ofeT := OfeT simple_type st_ofe_mixin.
+  Canonical Structure stO : ofeT := OfeT simple_type st_ofe_mixin.
 
   Global Instance st_own_ne n :
     Proper (dist n ==> eq ==> eq ==> dist n) st_own.
-- 
GitLab