bump gpfsl

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}%"]

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 Σ).

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 Σ).

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).