update dependencies

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

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

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