diff --git a/opam b/opam
index 836353ad251d4519c166de44a9d3bd99d212fdde..1e75e2c215ff3fe089cff1feae1eef4b0b5e9223 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 06e5ef4c6d26c07043bb5dd26359d5f12ce16217..b3076cfc543c54b48c0d755bb77b10c965b70953 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 9d1ad14cc561592fa84fed041e2a76d7f3ad1624..68c5d13a88060aea00f9c8f6fd7fc662d7856953 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 22223ab6eb8e84c40853eaab8fc14f387ccb032e..73c7c8dffee0c9c93955d5fe778723cf7d0348df 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).