From 58401ac2bf7046533f96a5b46cbe181aa74bc718 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Jun 2019 19:54:19 +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/examples/stack/refinement.v | 2 +-
 theories/lib/lock.v                  | 4 ++--
 theories/logic/model.v               | 4 ++--
 theories/logic/spec_ra.v             | 4 ++--
 theories/typing/fundamental.v        | 2 +-
 theories/typing/interp.v             | 8 ++++----
 7 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/opam b/opam
index a09613d..9d113d2 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-14.0.4032acd1") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index 0049631..f508754 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -21,7 +21,7 @@ Section proof.
     iSplitL "H1"; eauto with iFrame.
   Qed.
 
-  Notation D := (locC -n> valC -n> iProp Σ).
+  Notation D := (locO -n> valO -n> iProp Σ).
 
   Program Definition stack_link_pre (A : lrel Σ) : D -n> D := λne S v1 v2,
     (∃ w, (∃ q, v1 ↦{q} w) ∗
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index d6a3dfc..4036da7 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -15,8 +15,8 @@ Definition with_lock : val := λ: "e" "l" "x",
   let: "v" := "e" "x" in
   release "l";; "v".
 
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
+Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 89a1830..4b4f5a9 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -29,12 +29,12 @@ Section lrel_ofe.
   Instance lrel_equiv : Equiv (lrel Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
   Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lrel_ofe_mixin : OfeMixin (lrel Σ).
-  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -c> val -c> iProp Σ))). Qed.
+  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iProp Σ))). Qed.
   Canonical Structure lrelC := OfeT (lrel Σ) lrel_ofe_mixin.
 
   Global Instance lrel_cofe : Cofe lrelC.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -c> val -c> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
+    apply (iso_cofe_subtype' (λ A : val -d> val -d> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
     - apply _.
     - apply limit_preserving_forall=> w1.
       apply limit_preserving_forall=> w2.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index c2abfec..b605046 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -11,7 +11,7 @@ Definition relocN := nroot .@ "reloc".
 Definition specN := relocN .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
-Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).
+Definition tpoolUR : ucmraT := gmapUR nat (exclR exprO).
 Definition cfgUR := prodUR tpoolUR (gen_heapUR loc val).
 
 (** The CMRA for the thread pool. *)
@@ -107,7 +107,7 @@ Section conversions.
     - by rewrite lookup_insert tpool_lookup lookup_app_r // Nat.sub_diag.
     - rewrite lookup_insert_ne; last lia.
       rewrite !tpool_lookup ?lookup_ge_None_2 ?app_length //=;
-         change (ofe_car exprC) with expr; lia.
+         change (ofe_car exprO) with expr; lia.
   Qed.
 
   Lemma tpool_singleton_included tp j e :
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 2b2fce1..77ede4c 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -10,7 +10,7 @@ From Autosubst Require Import Autosubst.
 
 Section fundamental.
   Context `{relocG Σ}.
-  Implicit Types Δ : listC (lrelC Σ).
+  Implicit Types Δ : listO (lrelC Σ).
   Hint Resolve to_of_val.
 
   Local Ltac intro_clause := progress (iIntros (vs) "#Hvs /=").
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 021ff14..21cf35a 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -11,7 +11,7 @@ From Autosubst Require Import Autosubst.
 Section semtypes.
   Context `{relocG Σ}.
 
-  Program Definition ctx_lookup (x : var) : listC (lrelC Σ) -n> (lrelC Σ)
+  Program Definition ctx_lookup (x : var) : listO (lrelC Σ) -n> (lrelC Σ)
     := λne Δ, (from_option id lrel_true (Δ !! x))%I.
   Next Obligation.
     intros x n Δ Δ' HΔ.
@@ -25,8 +25,8 @@ Section semtypes.
       rewrite HP in HP'. inversion HP'.
   Qed.
 
-  Program Fixpoint interp (τ : type) : listC (lrelC Σ) -n> lrelC Σ :=
-    match τ as _ return listC (lrelC Σ) -n> lrelC Σ with
+  Program Fixpoint interp (τ : type) : listO (lrelC Σ) -n> lrelC Σ :=
+    match τ as _ return listO (lrelC Σ) -n> lrelC Σ with
     | TUnit => λne _, lrel_unit
     | TNat => λne _, lrel_int
     | TBool => λne _, lrel_bool
@@ -94,7 +94,7 @@ Section interp_ren.
     - intros v1 v2; simpl.
       rewrite iter_up. case_decide; simpl; properness.
       { by rewrite !lookup_app_l. }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia..].
       assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1))%nat as Hwat.
       { lia. }
-- 
GitLab