From a6c6c2ba64cb304d05f1476dfda2be1e95c86ef4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Apr 2020 09:05:25 +0200
Subject: [PATCH] update dependencies

---
 opam                                 |  2 +-
 theories/lang/arc.v                  |  2 +-
 theories/lifetime/model/borrow_sep.v |  2 +-
 theories/lifetime/model/primitive.v  | 14 +++++++-------
 theories/lifetime/model/reborrow.v   |  2 +-
 5 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/opam b/opam
index f59ccaba..f614c3b5 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-04-04.0.848c1c07") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-04-07.0.efcb9e71") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index a93cc909..f0c472fd 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -2692,7 +2692,7 @@ Section arc.
       iExists _. by iFrame "SD' SeenD'". }
 
     (* finally done with the CAS *)
-    iIntros "!>" (b t' [] v') "(IS &_& [([%[%_]]&R'&Q) | ([%_] &R'&Rs&_)])";
+    iIntros "!>" (b t' [] v') "(IS &_& [([% [% _]]&R'&Q) | ([% _] &R'&Rs&_)])";
       last first.
     { (* CAS failure case first *)
       subst b. rewrite 2!acq_sep_elim 3!acq_embed_elim.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 40f75c83..a3fcd0ea 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -155,7 +155,7 @@ Proof.
   iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
   { iIntros (->).
     iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
-    exfalso. revert Hj1j2. by rewrite /= op_singleton singleton_valid. }
+    exfalso. revert Hj1j2. by rewrite /= singleton_op singleton_valid. }
   iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
     as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
   { done. }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index f1d2c10e..1d98bb66 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -70,7 +70,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_valid op_singleton singleton_valid=> /agree_op_invL' <-.
+  rewrite auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_sep κ x x1 x2 :
@@ -102,7 +102,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_valid op_singleton singleton_valid=> /agree_op_invL' <-.
+  rewrite 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_sep κ x x1 x2 :
@@ -136,7 +136,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_sep κ x x1 x2 :
@@ -289,7 +289,7 @@ Proof.
   iDestruct 1 as (Λ' V')  "(% & #? & H')".
   iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
   iDestruct "H" as (V'') "[#? 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].
@@ -306,11 +306,11 @@ Proof.
   - iIntros "H". iDestruct "H" as (V') "[#? H] ".
     (* FIXME : the Proper instance for singleton cannot be found automatically here. *)
     rewrite (fin_maps.singletonM_proper Λ _ (Cinl (_, to_latT V' ⋅ to_latT V'))); last first.
-    { rewrite lat_op_join /= lat_join_idem //. } rewrite pair_op Cinl_op -op_singleton.
+    { rewrite lat_op_join /= lat_join_idem //. } rewrite pair_op Cinl_op -singleton_op.
     iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; auto.
   - iIntros "[Hp Hq]". iDestruct "Hp" as (Vp') "[#HVp' p]".
     iDestruct "Hq" as (Vq') "[#HVq' Hq]". iExists (_ ⊔ _).
-    rewrite -lat_op_join' pair_op Cinl_op -op_singleton auth_frag_op own_op.
+    rewrite -lat_op_join' pair_op Cinl_op -singleton_op auth_frag_op own_op.
     iFrame. iCombine "HVp' HVq'" as "HVpq'".
     iDestruct (monPred_in_intro with "HVpq'") as (V) "[HV [%%]]".
     rewrite (_:Vp' ⊔ Vq' ⊑ V) //. solve_lat.
@@ -324,7 +324,7 @@ Proof.
   rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sep.
   apply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
   rewrite (fin_maps.singletonM_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
-  { rewrite lat_op_join' right_id //. } rewrite pair_op Cinl_op -op_singleton.
+  { rewrite lat_op_join' right_id //. } rewrite pair_op Cinl_op -singleton_op.
   iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; [by auto|]. iIntros (?). iExists bot. auto.
 Qed.
 
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 771070fd..debb35eb 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -25,7 +25,7 @@ Proof.
   iIntros "(#Hag & Hσ & Hclose)". iSplitL "Hσ"; [by auto|]. iIntros "H".
   iApply "Hclose". iDestruct "H" as (γ') "[#Hag' H]".
   iDestruct (own_valid_2 with "Hag Hag'") as %Hγs. move : Hγs.
-  rewrite auth_frag_valid op_singleton singleton_valid=> /agree_op_invL' <- //.
+  rewrite auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <- //.
 Qed.
 
 Section reborrow.
-- 
GitLab