bump gpfsl

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

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 :=