From 26951be14eccb8133ee0d4f77f542a64cf249d6e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 1 Sep 2021 11:14:08 +0200
Subject: [PATCH] Bump.

---
 coq-lambda-rust.opam    | 2 +-
 theories/lang/lifting.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d061db51..bd2b84d4 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-07-29.1.13063825") | (= "dev") }
+  "coq-iris" { (= "dev.2021-09-01.0.55cd1cc9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index d337d48b..b67d3c12 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -12,13 +12,13 @@ Class lrustGS Σ := LRustGS {
 }.
 
 Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
-  iris_invG := lrustGS_invGS;
+  iris_invGS := lrustGS_invGS;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;
   num_laters_per_step _ := 0%nat;
   state_interp_mono _ _ _ _ := fupd_intro _ _
 }.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Ltac inv_lit :=
   repeat match goal with
-- 
GitLab