From e5165c7277ddab14ba6f1c80a3cdd2ddb986fff4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Sep 2019 19:43:49 +0200
Subject: [PATCH] Bump Iris.

---
 opam                                          | 2 +-
 theories/examples/stack/refinement.v          | 2 +-
 theories/experimental/helping/helping_stack.v | 2 +-
 theories/logic/model.v                        | 5 +++--
 theories/logic/spec_rules.v                   | 2 +-
 5 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/opam b/opam
index 2f519a3..26435f3 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" { (= "3.2.0") | (= "dev") }
+  "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c731587..f9444e3 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 := (locO -n> valO -n> iProp Σ).
+  Notation D := (locO -n> valO -n> iPropO Σ).
 
   Program Definition stack_link_pre (A : lrel Σ) : D -n> D := λne S v1 v2,
     (∃ w, (∃ q, v1 ↦{q} w) ∗
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index e0a3b69..376e0f9 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -221,7 +221,7 @@ Section refinement.
   Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
   Proof. intros [|][|]; simpl; congruence. Qed.
 
-  Local Notation D := (olocO -d> valO -d> iProp Σ).
+  Local Notation D := (olocO -d> valO -d> iPropO Σ).
 
   Definition stack_link_pre (A : lrel Σ) : D → D := λ S ol v2,
     match ol return _ with
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 0c3cfc4..057ce90 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -29,12 +29,13 @@ 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 -d> val -d> iProp Σ))). Qed.
+  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iPropO Σ))). Qed.
   Canonical Structure lrelC := OfeT (lrel Σ) lrel_ofe_mixin.
 
   Global Instance lrel_cofe : Cofe lrelC.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -d> val -d> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
+    apply (iso_cofe_subtype' (λ A : val -d> val -d> iPropO Σ,
+      ∀ 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_rules.v b/theories/logic/spec_rules.v
index 2db07ac..2849bfd 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -112,7 +112,7 @@ Section rules.
     { by eapply auth_update, prod_local_update_1,
          singleton_local_update, (exclusive_local_update _ (Excl (fill K #p))). }
     iExists p. iFrame. iApply "Hclose". iNext.
-    iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪) σ).
+    iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪.) σ).
     rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
-- 
GitLab