From 1b8cc687f56321326aed2667549be5a92efb87a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 30 Sep 2020 09:48:23 +0200
Subject: [PATCH] update dependencies; fix for auth change
---
opam | 2 +-
theories/utils/contribution.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index 4f214a0..f67977e 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
- "coq-iris" { (= "dev.2020-09-15.3.986a8883") | (= "dev") }
+ "coq-iris" { (= "dev.2020-09-30.0.fe735a96") | (= "dev") }
]
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index eae3ada..4615bd9 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -64,7 +64,7 @@ Section contribution.
Proof.
rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
iDestruct (own_valid_2 with "Hs Hc")
- as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid; first done.
+ as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
by destruct (Pos.lt_irrefl 1).
Qed.
@@ -89,7 +89,7 @@ Section contribution.
- iDestruct "Hs" as "(_ & _ & Hc')".
by iDestruct (own_valid_2 with "Hc Hc'") as %?.
- iDestruct (own_valid_2 with "Hs Hc")
- as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid.
+ as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
by destruct n.
--
GitLab