From 09f4b00d092f3156dd2f6ad9f410fd2358b091a3 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sun, 6 Sep 2020 01:23:03 +0200
Subject: [PATCH] update dependencies
---
opam | 2 +-
theories/logic/gps.v | 2 ++
theories/typing/lft_contexts.v | 2 ++
3 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/opam b/opam
index 0d07d0df..836353ad 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-09-05.0.a8e8ebf3") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-09-05.2.73f2f8a8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 68c5d13a..9d1ad14c 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -3,6 +3,8 @@ 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 73c7c8df..22223ab6 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -22,6 +22,8 @@ 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