diff --git a/opam b/opam
index 18b969071756fdf7b7bd3a8c7a09088fd651fd44..da0ac5ca8c018d0c8f4107ccce2fc5b259e31e2a 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-02-21.1.cabd1b87") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-02-26.0.d98b5c57") | (= "dev") }
 ]
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index c159ac596e23b2007b5fcfd1420e6ce41127124a..f5a95cb55b5b70dc57e2a162f2a81bd9528545a8 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -295,7 +295,7 @@ Proof.
 Qed.
 
 Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
-  (FIN: model.final_st s') (DISJ: histN ## N)
+  (FIN: final_st s') (DISJ: histN ## N)
   (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
   (RLX: o = Relaxed ∨ o = AcqRel) :
   let VS : vProp :=