diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 2d33a2f800a4869eaa041463bc3e0a0da2334211..f71b1606c76dddf5df049545fdf731b6ef1d2bb0 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-07-27.0.774a97d1") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-08-10.0.d486f5e1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index ce46d4fc1e1751acc6d38096613dbf8b7594346f..e1e398f1ca463953cdcc839b13508dd30def832e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -9,7 +9,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Class typePreG Σ := PreTypeG {
-  type_preG_heapG :> noprolPreG Σ;
+  type_preG_heapG :> noprolGpreS Σ;
   type_preG_lftG :> lftPreG Σ view_Lat;
   type_preG_na_invG :> na_invG view_Lat Σ;
   type_preG_frac_borG :> frac_borG Σ