From 94def2ba03a01ce05fab5c016ff16bdde75344ff Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 10 Aug 2021 13:43:12 +0200
Subject: [PATCH] Bump dependency

---
 coq-lambda-rust.opam        | 2 +-
 theories/typing/soundness.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 2d33a2f8..f71b1606 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 ce46d4fc..e1e398f1 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 Σ
-- 
GitLab