diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index e26604eaa97e23ddf8365d2b3d00ad1be18a3a0c..23fbdff87fc734fc52ff46a5587d8c13d4dc0e8d 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -219,7 +219,7 @@ Qed.
 (** This simpler form of adequacy requires the [irisGS] instance that you use
 everywhere to syntactically be of the form
 {|
-  iris_invG := ...;
+  iris_invGS := ...;
   state_interp σ _ κs _ := ...;
   fork_post v := ...;
   num_laters_per_step _ := 0;
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index ef838305f6eea1226366bb1e561505be9da76da7..859d053482cf8a9059a65fb1cf3e4bf21edeee84 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -21,13 +21,13 @@ Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
 }.
 
 Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
-  iris_invG := ownP_invG;
+  iris_invGS := ownP_invG;
   state_interp σ _ κs _ := own ownP_name (●E σ)%I;
   fork_post _ := True%I;
   num_laters_per_step _ := 0;
   state_interp_mono _ _ _ _ := fupd_intro _ _
 }.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Definition ownPΣ (Λ : language) : gFunctors :=
   #[invΣ;
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index db92ff28df23469153892dce60ee00074454089b..b918c293379f1c1bef06f481c0807cef1aa162eb 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invG :> invGS Σ;
+  iris_invGS :> invGS Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [Λstate] is the global state,
@@ -45,7 +45,7 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
   state_interp_mono σ ns κs nt:
     state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
 }.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index e70d0ff1d6ef35244236c21a63f27026f506768c..0af58af239b8cc83a7b465365026f62d84e440fb 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -11,14 +11,14 @@ From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
 
 Class heapGS Σ := HeapGS {
-  heapG_invG : invGS Σ;
-  heapG_gen_heapG :> gen_heapGS loc (option val) Σ;
-  heapG_inv_heapG :> inv_heapGS loc (option val) Σ;
-  heapG_proph_mapG :> proph_mapGS proph_id (val * val) Σ;
+  heapGS_invGS : invGS Σ;
+  heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
+  heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
+  heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
 }.
 
-Global Instance heapG_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
-  iris_invG := heapG_invG;
+Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
+  iris_invGS := heapGS_invGS;
   state_interp σ _ κs _ :=
     (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
   fork_post _ := True%I;