From 4ce78761937ccada863fb4cda56d486804c048dc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Oct 2020 08:59:03 +0200
Subject: [PATCH] update dependencies; fix for auth changes
---
opam | 2 +-
theories/lang/arc_cmra.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index d57c87b2..e41b3f1e 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-10-13.0.65e2d7ca") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-10-21.0.e29403ca") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index ec4e06cd..81a09112 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -366,7 +366,7 @@ Section ArcGhost.
iDestruct 1 as (Ut) "WU". iIntros "WU'".
iDestruct (WkUps_join with "[$WU $WU']") as "WU".
iDestruct (@own_valid _ arcUR with "WU")
- as %[_ [_ [[VAL _]%auth_frag_valid _]]].
+ as %[_ [_ [[VAL _]%auth_frag_valid_1 _]]].
iPureIntro. simpl in VAL.
have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
@@ -583,7 +583,7 @@ Section ArcGhost.
iDestruct 1 as (Mt) "SM". iIntros "SM'".
iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt'.
iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
- iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _] _] _] _]].
+ iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _]%auth_frag_valid_1 _] _] _]].
iPureIntro. simpl in VAL.
have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
--
GitLab