From 6c1311a1542df63c312f719ad5b16017222ac6f6 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 15 Sep 2020 10:35:17 +0200 Subject: [PATCH] update dependencies; fix for agree_op rename --- opam | 2 +- theories/lang/arc_cmra.v | 2 +- theories/lifetime/model/primitive.v | 6 +++--- theories/lifetime/model/reborrow.v | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/opam b/opam index 1e75e2c2..36332e3a 100644 --- a/opam +++ b/opam @@ -16,7 +16,7 @@ This branch uses a proper weak memory model. """ depends: [ - "coq-gpfsl" { (= "dev.2020-09-06.0.570c82c9") | (= "dev") } + "coq-gpfsl" { (= "dev.2020-09-15.0.f118e18e") | (= "dev") } ] build: [make "-j%{jobs}%"] diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v index 07ec46d1..ce111fe8 100644 --- a/theories/lang/arc_cmra.v +++ b/theories/lang/arc_cmra.v @@ -220,7 +220,7 @@ Section ArcGhost. iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro. move : VAL => [/=_ [/= [[VAL _]_]_]]. move :VAL. rewrite /= -auth_frag_op -Some_op -pair_op auth_valid_discrete /= Some_valid. - move => [_ /agree_op_inv' /to_latT_inj /leibniz_equiv_iff // ]. + move => [_ /to_agree_op_inv /to_latT_inj /leibniz_equiv_iff // ]. Qed. Lemma StrongMoveAuth_Cert_include γ Mt Mt': diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v index bcda1f20..fb9343ca 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 singleton_op singleton_valid=> /agree_op_invL' <-. + rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-. 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 singleton_op singleton_valid=> /agree_op_invL' <-. + rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-. 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 singleton_op singleton_valid=> /agree_op_invL' <-. + rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-. iExists γs. iSplit. done. rewrite own_op; iFrame. Qed. Global Instance own_inh_into_sep κ x x1 x2 : diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v index 0622b412..6f79fbc2 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 singleton_op singleton_valid=> /agree_op_invL' <- //. + rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <- //. Qed. Section reborrow. -- GitLab