diff --git a/tests/atomic.ref b/tests/atomic.ref
index 859bb6deb7e32902cf459b362c807d7e09ea45b6..8bf105a88b974cce1d8b3ddbf9551365d7851f48 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   aheap : atomic_heap Σ
   Q : iProp Σ
   l : loc
@@ -23,14 +23,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
   ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -41,7 +41,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -55,14 +55,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -73,7 +73,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -86,14 +86,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -104,7 +104,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -118,14 +118,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -136,7 +136,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -151,7 +151,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
@@ -160,7 +160,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -172,7 +172,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
@@ -181,7 +181,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -193,7 +193,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
@@ -203,7 +203,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -217,7 +217,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
@@ -226,7 +226,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -238,7 +238,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   ============================
@@ -248,7 +248,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   Φ : language.val heap_lang → iProp Σ
@@ -261,7 +261,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   ============================
@@ -271,7 +271,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   Φ : language.val heap_lang → iProp Σ
@@ -284,7 +284,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   ============================
@@ -294,7 +294,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
@@ -307,7 +307,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   ============================
@@ -318,7 +318,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
@@ -334,7 +334,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 64e37382064e716331fc28ad29f4b1d9f4bea613..e5af6aef4d1abfa468a63f4a5dd6a2630fcba346 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -3,7 +3,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   ============================
   --------------------------------------∗
@@ -12,7 +12,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l : loc
   ============================
@@ -25,7 +25,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l : loc
   ============================
@@ -37,7 +37,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l, l' : loc
   ============================
@@ -51,7 +51,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   _ : ▷ l ↦ #0
@@ -61,7 +61,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   _ : l ↦ #1
@@ -97,7 +97,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   "Hl1" : l ↦{#1 / 2} #0
@@ -108,7 +108,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   --------------------------------------∗
@@ -122,7 +122,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   ============================
   --------------------------------------∗
   WP "x" {{ _, True }}
@@ -130,7 +130,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   n : Z
   H : (0 < n)%Z
   Φ : val → iPropI Σ
@@ -146,7 +146,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   vs : list val
   ============================
@@ -160,7 +160,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   v : val
   ============================
   --------------------------------------∗
@@ -171,7 +171,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   v : val
   ============================
   --------------------------------------∗
@@ -180,7 +180,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   v : val
   Φ : val → iPropI Σ
@@ -194,7 +194,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   dq : dfrac
   l : loc
   v : val
@@ -208,7 +208,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   I : val → Prop
   Heq : ∀ v : val, I v ↔ I #true
@@ -219,7 +219,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E1, E2 : coPset
   P : iProp Σ
   ============================
@@ -235,7 +235,7 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   N : namespace
   E : coPset
   P : iProp Σ
@@ -254,7 +254,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   N : namespace
   E : coPset
   P : iProp Σ
@@ -270,7 +270,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   ============================
   --------------------------------------∗
   WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
@@ -278,7 +278,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
@@ -290,7 +290,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   ============================
@@ -303,7 +303,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   E : coPset
@@ -317,7 +317,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}
diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index dff62fa87c541d8a9c6fd3ef8e0197c946d5bf88..1c677e63f410219d4b8a5dc654cfb13f0e4dfd42 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,14 +1,14 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P, Q : iProp Σ
   ============================
   P ={⊤}=∗ Q
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 74a366e9c6f993d80297e8e81cce620007254729..d7ba9448abfccedb64306a3210c46f8a8568b2ab 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -66,7 +66,7 @@ P
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   counterG0 : counterG Σ
   l : loc
   n : nat
@@ -82,7 +82,7 @@ P
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   counterG0 : counterG Σ
   l : loc
   n : nat
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index b92601d2c985bc7b8030798397c05f7b8be60bac..cd47ff4bdd1763eb219c002b3b74f50dd5d0308e 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   hd, acc : val
   xs, ys : list val
   Φ : val → iPropI Σ
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   acc : val
   ys : list val
   Φ : val → iPropI Σ
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index 182ac473defb6f95ccc9eee57e01c738df35bc55..94a3ddc05772f1ed1db1cd01a26a0c45d7698dfc 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
diff --git a/tests/one_shot_once.ref b/tests/one_shot_once.ref
index 686937f1065150df00ae611d3f68801822a9a8bf..4be43be0dc1b52d1098fb69503a0791d46ee5469 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index 6c4fc6ad6fd4fb1001b0273627b8c254c91355cc..b0d84bf2c75c5d4b125f57031d216c7197c7210e 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -49,7 +49,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -68,7 +68,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -89,7 +89,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -120,7 +120,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -136,7 +136,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index dc20ed5696e88438d41e445c85d2448de207cd53..d049912e274832e8df70839ebb36fa384e240c9a 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -43,7 +43,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -61,7 +61,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -80,7 +80,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -101,7 +101,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -115,7 +115,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -146,7 +146,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -160,7 +160,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -175,7 +175,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -191,7 +191,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index be3c1169d610c66856153aa4fc6a107a03c0e9ac..4d1d96175d23bf8ca564feaab67ade0c4dde7c9a 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -63,7 +63,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   N : namespace
   𝓟 : iProp Σ
   ============================
@@ -76,7 +76,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   N : namespace
   𝓟 : iProp Σ
   ============================