diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d061db512451ec32f728301e696dfe1481ec837e..bd2b84d4c81f7cd317e89b9a269fdc44eda3c8f9 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 d337d48bb095df84894216bf8e0ce3e23616a047..b67d3c12c6ea524abb70d60a18d64406b084eeb4 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