From fce2b7355372c28fa1ade719b1872748ebd4bbd4 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 17 Dec 2019 10:04:52 +0100
Subject: [PATCH] bump gpfsl
---
opam | 2 +-
theories/lang/arc.v | 10 +++++-----
theories/lang/spawn.v | 2 +-
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/opam b/opam
index e4fc5bc7..875c0e14 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-gpfsl" { (= "dev.2019-12-10.0.c3e8211e") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2019-12-16.1.573302f9") | (= "dev") }
]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 1696ed6e..426e806a 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -290,8 +290,8 @@ Section arc.
Proper (pointwise_relation _ (dist n) ==> dist n ==>
eq ==> eq ==> eq ==> eq ==> eq ==> dist n) arc_inv.
Proof.
- move => ?????????????????????. subst.
- apply bi.sep_ne; [done|]. apply bi.sep_ne; apply GPS_INV_ne.
+ repeat intro. subst.
+ apply bi.sep_ne; [done|]. apply bi.sep_ne; apply GPS_INV_ne; [|done| |done].
- move => b ?????. apply bi.exist_ne => st.
apply bi.sep_ne; [done|]. destruct b; [|done]. apply bi.sep_ne; [done|].
destruct st as [[]|]; [|done]. solve_proper.
@@ -305,7 +305,7 @@ Section arc.
eq ==> eq ==> eq ==> eq ==> eq ==> (≡))
arc_inv.
Proof.
- move => ?????????????????????. subst.
+ repeat intro. subst.
apply bi.sep_proper; [done|].
apply bi.sep_proper; apply GPS_INV_proper; auto;
move => b ?????; apply bi.exist_proper => ?; solve_proper.
@@ -316,7 +316,7 @@ Section arc.
eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> dist n)
is_arc.
Proof.
- move => ????????????????????????. subst. constructor => ?.
+ repeat intro. subst. constructor => ?.
rewrite /is_arc. apply view_inv_contractive.
destruct n; [done|by apply arc_inv_ne].
Qed.
@@ -325,7 +325,7 @@ Section arc.
Proper (pointwise_relation _ (≡) ==> (≡) ==> eq
==> eq ==> eq ==> eq ==> eq ==> eq ==> (≡)) is_arc.
Proof.
- move => ????????????????????????. subst.
+ repeat intro. subst.
by apply view_inv_proper, arc_inv_proper.
Qed.
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 7ef91fc4..19a617f9 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -75,7 +75,7 @@ Global Instance finish_handle_contractive n γc γe c :
Proof.
move => ???. do 3 (apply bi.exist_ne => ?).
apply bi.sep_ne; [done|]. apply bi.sep_ne; [|done].
- apply GPS_vSP_Writer_contractive. destruct n; [done|].
+ apply GPS_vSP_Writer_contractive; [|done]. destruct n; [done|].
simpl => ??????. apply bi.exist_ne => b'.
apply bi.sep_ne; [done|]. destruct b'; [|done]. solve_proper.
Qed.
--
GitLab