From 36a7f77cfbd2d99153882ddef6d80cb913799433 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Oct 2020 13:29:13 +0200
Subject: [PATCH] update dependencies; fix unification problems
---
opam | 2 +-
theories/lang/arc_cmra.v | 6 +++---
theories/typing/lib/rc/rc.v | 2 +-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/opam b/opam
index 203be240..d57c87b2 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-10-10.1.4e05b3e8") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-10-13.0.65e2d7ca") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 55b606b0..ec4e06cd 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -436,7 +436,7 @@ Section ArcGhost.
iMod (@own_update _ arcUR with "own") as "$"; [|done].
apply prod_update; simpl; [|by rewrite right_id].
apply prod_update; simpl; [|done]. apply auth_update_alloc.
- rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
+ rewrite /= -(right_id None op (Some _)). by apply: op_local_update_discrete.
Qed.
Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
@@ -496,7 +496,7 @@ Section ArcGhost.
apply prod_update; simpl; [|by rewrite right_id].
apply prod_update; simpl; [|done].
apply auth_update_dealloc. rewrite /= -(right_id None op (Some _)).
- apply cancel_local_update_unit, _.
+ apply: cancel_local_update_unit.
Qed.
Lemma StrongAuth_drop γ q q' n:
@@ -519,7 +519,7 @@ Section ArcGhost.
iMod (@own_update _ arcUR with "own") as "$"; [|done].
apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
apply auth_update_dealloc. apply prod_local_update; [done|].
- rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+ rewrite /= -(right_id None op (Some _)). apply: cancel_local_update_unit.
Qed.
Lemma WeakAuth_drop γ iS (q q': frac) n:
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 5dc181dc..6fa28d52 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -365,7 +365,7 @@ Section code.
{ by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
iMod (own_update_2 with "Hst Htok") as "$"; last done.
apply auth_update_dealloc, prod_local_update', reflexivity.
- rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_unit, _.
+ rewrite -{1}(right_id None _ (Some _)). apply: cancel_local_update_unit.
+ apply csum_included in Hincl.
destruct Hincl as [->|[(?&(?,?)&[=<-]&->&(q',strong)&[]%(inj2 pair))|
(?&?&[=]&?)]]; first done. setoid_subst.
--
GitLab