From 166021b3c909fac6f5d1df2cc1ac182d31571d33 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 26 Feb 2019 16:03:36 +0100
Subject: [PATCH] bump gpfsl
---
opam | 2 +-
theories/logic/gps.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 18b96907..da0ac5ca 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-02-21.1.cabd1b87") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2019-02-26.0.d98b5c57") | (= "dev") }
]
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index c159ac59..f5a95cb5 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -295,7 +295,7 @@ Proof.
Qed.
Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
- (FIN: model.final_st s') (DISJ: histN ## N)
+ (FIN: final_st s') (DISJ: histN ## N)
(SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
(RLX: o = Relaxed ∨ o = AcqRel) :
let VS : vProp :=
--
GitLab