From b4b5bee3e3930bfb925ff4b0800bffaa6999603e Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 7 Sep 2020 00:01:23 +0200
Subject: [PATCH] bump gpfsl
---
opam | 2 +-
theories/lang/lock.v | 2 +-
theories/logic/gps.v | 2 --
theories/typing/lft_contexts.v | 2 --
4 files changed, 2 insertions(+), 6 deletions(-)
diff --git a/opam b/opam
index 836353ad..1e75e2c2 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-09-05.2.73f2f8a8") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-09-06.0.570c82c9") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 06e5ef4c..b3076cfc 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -27,7 +27,7 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
Section proof.
- Context `{noprolG Σ, !lftG (view_Lat loc) (↑histN) Σ, lockG Σ}.
+ Context `{noprolG Σ, !lftG view_Lat (↑histN) Σ, lockG Σ}.
Implicit Types (l : loc).
Local Notation vProp := (vProp Σ).
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 9d1ad14c..68c5d13a 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -3,8 +3,6 @@ From lrust.lang Require Import notation.
From lrust.lifetime Require Import at_borrow.
From gpfsl.gps Require Import middleware.
-Notation view_Lat := (view_Lat loc).
-
Section gps_at_bor_SP.
Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG view_Lat (↑histN) Σ} (N: namespace).
Local Notation vProp := (vProp Σ).
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 22223ab6..73c7c8df 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -22,8 +22,6 @@ Notation llctx := (list llctx_elt).
Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
-Notation view_Lat := (view_Lat loc).
-
Section lft_contexts.
Context `{!invG Σ, !lftG view_Lat (↑histN) Σ}.
Implicit Type (κ : lft).
--
GitLab