diff --git a/opam b/opam
index 0d07d0dfcbc15d4d9a5fc0094d45de71216f8774..836353ad251d4519c166de44a9d3bd99d212fdde 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 68c5d13a88060aea00f9c8f6fd7fc662d7856953..9d1ad14cc561592fa84fed041e2a76d7f3ad1624 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 73c7c8dffee0c9c93955d5fe778723cf7d0348df..22223ab6eb8e84c40853eaab8fc14f387ccb032e 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).