From a6b87eb4b0374f2670ca5ec02fcc122feedbd35b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Apr 2020 19:00:02 +0200
Subject: [PATCH] fix for Iris renames

---
 theories/lang/heap.v                 |  6 +++---
 theories/lifetime/model/borrow_sep.v |  2 +-
 theories/lifetime/model/primitive.v  | 12 ++++++------
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 2cc7ebc3..3ad8e893 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -118,7 +118,7 @@ Section heap.
   Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
   Proof.
     intros p q.
-    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton -pair_op agree_idemp.
+    by rewrite heap_mapsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
   Qed.
   Global Instance heap_mapsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
@@ -143,7 +143,7 @@ Section heap.
   Proof.
     rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
     eapply pure_elim; [done|]=> /auth_frag_valid /=.
-    rewrite op_singleton -pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
+    rewrite singleton_op -pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
 
   Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
@@ -272,7 +272,7 @@ Section heap.
     †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
-      op_singleton -pair_op inter_op.
+      singleton_op -pair_op inter_op.
   Qed.
 
   (** Properties about heap_freeable_rel and heap_freeable *)
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index b1914199..663e7c01 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -99,7 +99,7 @@ Proof.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
     { iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
       iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
-      exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
+      exfalso. revert Hj1j2. rewrite /= singleton_op singleton_valid.
       by intros [[]]. }
     iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
       as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 56fc8a6f..4429a175 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -66,7 +66,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
-  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL' <-.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
@@ -100,7 +100,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
-  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
@@ -134,7 +134,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
-  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
@@ -277,7 +277,7 @@ Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
   iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
   iDestruct (own_valid_2 with "H H'") as %Hvalid.
-  move: Hvalid=> /auth_frag_valid /=; by rewrite op_singleton singleton_valid.
+  move: Hvalid=> /auth_frag_valid /=; by rewrite singleton_op singleton_valid.
 Qed.
 
 Lemma lft_tok_static q : ⊢ q.[static].
@@ -290,7 +290,7 @@ Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.
   intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper.
-  intros Λ ?. rewrite Cinl_op -op_singleton auth_frag_op own_op //.
+  intros Λ ?. rewrite Cinl_op -singleton_op auth_frag_op own_op //.
 Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
@@ -298,7 +298,7 @@ Proof. split. done. apply _. Qed.
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
-  rewrite -auth_frag_op op_singleton -pair_op agree_idemp. done.
+  rewrite -auth_frag_op singleton_op -pair_op agree_idemp. done.
 Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-- 
GitLab