diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 1e928326883f6a7dfac777ca4acb7721d1f25dd0..6ea0fe6a5f5e70213e9af482b65309f8124f5a55 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -18,7 +18,7 @@ Global Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.
-  Context `{!invGS Σ, !boxG Σ} (N : namespace).
+  Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
 
   Definition slice_name := gname.
 
@@ -47,7 +47,7 @@ Global Instance: Params (@slice) 5 := {}.
 Global Instance: Params (@box) 5 := {}.
 
 Section box.
-Context `{!invGS Σ, !boxG Σ} (N : namespace).
+Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 5eba9f038fa85248333233cf78eef5d888ed7a14..bd26b84d022fa5a653ff59583d8cb093f7611151 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -14,7 +14,7 @@ Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{!invGS Σ, !cinvG Σ}.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -25,7 +25,7 @@ End defs.
 Global Instance: Params (@cinv) 5 := {}.
 
 Section proofs.
-  Context `{!invGS Σ, !cinvG Σ}.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 510986781c20b5e1e5d102ebc7eacb1e26e80469..120a6cca554352fbd4ae52ac4303a9d18d124003 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -15,23 +15,23 @@ Import le_upd_if.
     the interaction laws with the plainly modality in [BiFUpdPlainly]. While these laws are
     seldomly used, support for them is required for backwards compatibility.
 
-    Thus, we define two typeclasses [HasLc] and [HasNoLc].
-    The availability of the rules for later credits or the plainly interaction depends
-    on having an instance of the right one of these classes in the context. See below.
+    Thus, the [invGS_gen] typeclass ("gen" for "generalized") is parameterized by
+    a parameter of type [has_lc] that determines whether later credits are
+    available or not. [invGS] is provided as a convenient notation for the default [HasLc].
+    We don't use that notation in this file to avoid confusion.
  *)
+Inductive has_lc := HasLc | HasNoLc.
 
 Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
   invGpreS_wsat : wsatGpreS Σ;
   invGpreS_lc : lcGpreS Σ;
 }.
 
-Class invGS (Σ : gFunctors) : Set := InvG {
+Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
   invGS_wsat : wsatGS Σ;
   invGS_lc : lcGS Σ;
-  (* flag determining whether the fancy update allows later credit elimination *)
-  invGS_use_credits : bool;
 }.
-Global Hint Mode invGS - : typeclass_instances.
+Global Hint Mode invGS_gen - - : typeclass_instances.
 Global Hint Mode invGpreS - : typeclass_instances.
 Local Existing Instances invGpreS_wsat invGpreS_lc.
 (* [invGS_lc] needs to be global in order to enable the use of lemmas like [lc_split]
@@ -39,30 +39,22 @@ Local Existing Instances invGpreS_wsat invGpreS_lc.
    [invGS_wsat] also needs to be global as the lemmas in [invariants.v] require it. *)
 Global Existing Instances invGS_lc invGS_wsat.
 
+Notation invGS := (invGS_gen HasLc).
+
 Definition invΣ : gFunctors :=
   #[wsatΣ; lcΣ].
 Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
 Proof. solve_inG. Qed.
 
-(** [HasLc] asserts that the fancy update is defined with support for later credits. *)
-Class HasLc (Σ : gFunctors) `{!invGS Σ} :=
-  { has_credits : invGS_use_credits = true }.
-Global Hint Mode HasLc - - : typeclass_instances.
-(** [HasNoLc] asserts that the fancy update is defined without support for later credits,
-    but in turn supports the plainly interaction laws [BiFUpdPlainly]. *)
-Class HasNoLc (Σ : gFunctors) `{!invGS Σ} :=
-  { has_no_credits : invGS_use_credits = false }.
-Global Hint Mode HasNoLc - - : typeclass_instances.
-
-Local Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
-  wsat ∗ ownE E1 -∗ le_upd_if invGS_use_credits (◇ (wsat ∗ ownE E2 ∗ P)).
+Local Definition uPred_fupd_def `{!invGS_gen hlc Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+  wsat ∗ ownE E1 -∗ le_upd_if (if hlc is HasLc then true else false) (◇ (wsat ∗ ownE E2 ∗ P)).
 Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
-Global Arguments uPred_fupd {Σ _}.
-Local Lemma uPred_fupd_unseal `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Global Arguments uPred_fupd {hlc Σ _}.
+Local Lemma uPred_fupd_unseal `{!invGS_gen hlc Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
-Lemma uPred_fupd_mixin `{!invGS Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{!invGS_gen hlc Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
 Proof.
   split.
   - rewrite uPred_fupd_unseal. solve_proper.
@@ -82,18 +74,18 @@ Proof.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
 Qed.
-Global Instance uPred_bi_fupd `{!invGS Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+Global Instance uPred_bi_fupd `{!invGS_gen hlc Σ} : BiFUpd (uPredI (iResUR Σ)) :=
   {| bi_fupd_mixin := uPred_fupd_mixin |}.
 
-Global Instance uPred_bi_bupd_fupd `{!invGS Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Global Instance uPred_bi_bupd_fupd `{!invGS_gen hlc Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
 Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
 
 (** The interaction laws with the plainly modality are only supported when
   we opt out of the support for later credits. *)
-Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS Σ, !HasNoLc Σ} :
+Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS_gen HasNoLc Σ} :
   BiFUpdPlainly (uPredI (iResUR Σ)).
 Proof.
-  split; rewrite uPred_fupd_unseal /uPred_fupd_def has_no_credits.
+  split; rewrite uPred_fupd_unseal /uPred_fupd_def.
   - iIntros (E P) "H [Hw HE]".
     iAssert (â—‡ â–  P)%I as "#>HP".
     { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
@@ -116,25 +108,25 @@ Qed.
   these cannot be used for anything. They are merely provided to enable making
   the adequacy proof generic in whether later credits are used. *)
 Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} m :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
   (* We don't actually want any credits, but we need the [lcGS]. *)
   iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hc]".
-  set (Hi := InvG _ Hw Hc false).
+  set (Hi := InvG HasNoLc _ Hw Hc).
   iAssert (|={⊤,E2}=> P)%I with "[Hc]" as "H" .
-  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. by constructor. }
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. }
   rewrite uPred_fupd_unseal /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
 Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} φ n m :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ m)=> Hinv hc. iIntros "Hc".
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   iApply fupd_plainly_mask_empty. iSpecialize ("H" with "Hc").
   iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
@@ -143,10 +135,10 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} φ n m :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv Hc.
+  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
   iIntros "Hcred". destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
    simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
@@ -160,11 +152,11 @@ Qed.
   This is typically used as [iMod (lc_fupd_elim_later with "Hcredit HP") as "HP".],
   where ["Hcredit"] is a credit available in the context and ["HP"] is the
   assumption from which a later should be stripped. *)
-Lemma lc_fupd_elim_later `{!invGS Σ} `{!HasLc Σ} E P :
+Lemma lc_fupd_elim_later `{!invGS_gen HasLc Σ} E P :
    £ 1 -∗ (▷ P) -∗ |={E}=> P.
 Proof.
   iIntros "Hf Hupd".
-  rewrite uPred_fupd_unseal /uPred_fupd_def has_credits.
+  rewrite uPred_fupd_unseal /uPred_fupd_def.
   iIntros "[$ $]". iApply (le_upd_later with "Hf").
   iNext. by iModIntro.
 Qed.
@@ -173,7 +165,7 @@ Qed.
   in front of it in exchange for a later credit.
   This is typically used as [iApply (lc_fupd_add_later with "Hcredit")],
   where ["Hcredit"] is a credit available in the context. *)
-Lemma lc_fupd_add_later `{!invGS Σ} `{!HasLc Σ} E1 E2 P :
+Lemma lc_fupd_add_later `{!invGS_gen HasLc Σ} E1 E2 P :
   £ 1 -∗ (▷ |={E1, E2}=> P) -∗ |={E1, E2}=> P.
 Proof.
   iIntros "Hf Hupd". iApply (fupd_trans E1 E1).
@@ -181,13 +173,13 @@ Proof.
 Qed.
 
 Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 φ :
-  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> ⌜φ⌝) → φ.
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> ⌜φ⌝) → φ.
 Proof.
   iIntros (Hfupd). eapply (lc_soundness (S n)). intros Hc.
   rewrite lc_succ.
   iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
   iMod wsat_alloc as (Hw) "[Hw HE]".
-  set (Hi := InvG _ Hw Hc true).
+  set (Hi := InvG HasLc _ Hw Hc).
   iAssert (|={⊤,E2}=> ⌜φ⌝)%I with "[Hn]" as "H".
   { iMod (fupd_mask_subseteq E1) as "_"; first done. by iApply (Hfupd Hi). }
   rewrite uPred_fupd_unseal /uPred_fupd_def.
@@ -198,11 +190,11 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_lc `{!invGpreS Σ} φ n m :
-  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter. eapply (fupd_soundness_lc (m + n)); [apply _..|].
-  iIntros (Hinv Hc) "Hlc". rewrite lc_split.
+  iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
   clear Hiter.
   iInduction n as [|n] "IH"; simpl.
@@ -213,11 +205,11 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} φ n m :
-  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+  (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter. eapply (fupd_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
-  iIntros (Hinv Hc) "Hlc". rewrite lc_split.
+  iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
   clear Hiter.
   iInduction n as [|n] "IH"; simpl.
@@ -229,13 +221,12 @@ Qed.
 
 (** Generic soundness lemma for the fancy update, parameterized by [use_credits]
   on whether to use credits or not. *)
-Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (φ : Prop)
-    (use_credits : bool) (n m : nat) :
-  (∀ `{Hinv : invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (φ : Prop) (hlc : has_lc) (n m : nat) :
+  (∀ `{Hinv : invGS_gen hlc Σ},
     £ m ={⊤,∅}=∗ |={∅}▷=>^n ⌜φ⌝) →
   φ.
 Proof.
-  destruct use_credits.
+  destruct hlc.
   - apply step_fupdN_soundness_lc.
   - apply step_fupdN_soundness_no_lc.
 Qed.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 127ae29235bb2b19e55a2c8b233b0b57e026a6db..d88c997566f8787fe9764f55d19d68082c947eae 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -52,7 +52,7 @@ Proof. solve_inG. Qed.
 
 Section definitions.
   Context {L V : Type} `{Countable L}.
-  Context `{!invGS Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
+  Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
 
   Definition inv_heap_inv_P : iProp Σ :=
     ∃ h : gmap L (V * (V -d> PropO)),
@@ -77,7 +77,7 @@ Local Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
 
 (* [inv_heap_inv] has no parameters to infer the types from, so we need to
    make them explicit. *)
-Global Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
+Global Arguments inv_heap_inv _ _ {_ _ _ _ _ _ _}.
 
 Global Instance: Params (@inv_mapsto_own) 8 := {}.
 Global Instance: Params (@inv_mapsto) 7 := {}.
@@ -114,7 +114,7 @@ Section to_inv_heap.
   Qed.
 End to_inv_heap.
 
-Lemma inv_heap_init (L V : Type) `{Countable L, !invGS Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
+Lemma inv_heap_init (L V : Type) `{Countable L, !invGS_gen hlc Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
   ⊢ |==> ∃ _ : inv_heapGS L V Σ, |={E}=> inv_heap_inv L V.
 Proof.
   iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
@@ -128,7 +128,7 @@ Qed.
 
 Section inv_heap.
   Context {L V : Type} `{Countable L}.
-  Context `{!invGS Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
+  Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
   Implicit Types (l : L) (v : V) (I : V → Prop).
   Implicit Types (h : gmap L (V * (V -d> PropO))).
 
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index 3da0873656a13693ddd6209de1fae51079e7c660..ab012c825e6f3c4da4251a78e97f6a471fc8ffb6 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -8,17 +8,17 @@ Import uPred.
 Import le_upd_if.
 
 (** Semantic Invariants *)
-Local Definition inv_def `{!invGS Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Local Definition inv_def `{!invGS_gen hlc Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Local Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv := inv_aux.(unseal).
-Global Arguments inv {Σ _} N P.
+Global Arguments inv {hlc Σ _} N P.
 Local Definition inv_unseal : @inv = @inv_def := inv_aux.(seal_eq).
 Global Instance: Params (@inv) 3 := {}.
 
 (** * Invariants *)
 Section inv.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
   Implicit Types i : positive.
   Implicit Types N : namespace.
   Implicit Types E : coPset.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index c6b701d92c90321c8ad983e0b4baf2df4cecd001..627c41865e389c8287a331a8a89b428df0e09792 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -18,7 +18,7 @@ Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{!invGS Σ, !na_invG Σ}.
+  Context `{!invGS_gen hlc Σ, !na_invG Σ}.
 
   Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
     own p (CoPset E, GSet ∅).
@@ -32,7 +32,7 @@ Global Instance: Params (@na_inv) 3 := {}.
 Typeclasses Opaque na_own na_inv.
 
 Section proofs.
-  Context `{!invGS Σ, !na_invG Σ}.
+  Context `{!invGS_gen hlc Σ, !na_invG Σ}.
 
   Global Instance na_own_timeless p E : Timeless (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 64226cef5faaf4d86839335a5731f4d6ac4fb3d0..bf9cd4c33faa2bc8054d682983e4e54d52346a33 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -9,7 +9,7 @@ Import uPred.
 we prove a number of auxilary results. *)
 
 Section adequacy.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen hlc Λ Σ}.
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -137,15 +137,15 @@ Proof.
 Qed.
 End adequacy.
 
-Local Lemma wp_progress_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 e2
+Local Lemma wp_progress_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 e2
         (num_laters_per_step : nat → nat)  :
-    (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+    (∀ `{Hinv : !invGS_gen hlc Σ},
     ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
          (fork_post : val Λ → iProp Σ)
          state_interp_mono,
-       let _ : irisGS Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+       let _ : irisGS_gen hlc Λ Σ := IrisG Hinv stateI fork_post num_laters_per_step
                                   state_interp_mono
        in
        stateI σ1 0 κs 0 ∗
@@ -155,13 +155,13 @@ Local Lemma wp_progress_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} es σ1 n
   not_stuck e2 σ2.
 Proof.
   iIntros (Hwp ??).
-  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
-  iIntros (Hinv Hc) "Hcred".
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)"; first done.
+  iIntros (Hinv) "Hcred".
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
-  iMod (@wptp_progress _ _
-       (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
+  iMod (@wptp_progress _ _ _
+       (IrisG Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
     with "[Hσ] Hcred  Hwp") as "H"; [done| done |by rewrite right_id_L|].
   iAssert (|={∅}▷=>^(steps_sum num_laters_per_step 0 n) |={∅}=> ⌜not_stuck e2 σ2⌝)%I
     with "[-]" as "H"; last first.
@@ -169,14 +169,13 @@ Proof.
   iApply (step_fupdN_wand with "H"). iIntros "$".
 Qed.
 
-
 (** Iris's generic adequacy result *)
 (** The lemma is parameterized by [use_credits] over whether to make later credits available or not.
   Below, two specific instances are provided. *)
-Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1 n κs t2 σ2 φ
+Lemma wp_strong_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s es σ1 n κs t2 σ2 φ
         (num_laters_per_step : nat → nat) :
   (* WP *)
-  (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+  (∀ `{Hinv : !invGS_gen hlc Σ},
       ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
@@ -184,7 +183,7 @@ Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1
          (* Note: existentially quantifying over Iris goal! [iExists _] should
          usually work. *)
          state_interp_mono,
-       let _ : irisGS Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+       let _ : irisGS_gen hlc Λ Σ := IrisG Hinv stateI fork_post num_laters_per_step
                                   state_interp_mono
        in
        stateI σ1 0 κs 0 ∗
@@ -213,13 +212,13 @@ Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1
   φ.
 Proof.
   iIntros (Hwp ?).
-  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
-  iIntros (Hinv Hc) "Hcred".
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
+  iIntros (Hinv) "Hcred".
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
-  iMod (@wptp_strong_adequacy _ _
-       (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
+  iMod (@wptp_strong_adequacy _ _ _
+       (IrisG Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
     with "[Hσ] Hcred Hwp") as "H"; [done|by rewrite right_id_L|].
   iAssert (|={∅}▷=>^(steps_sum num_laters_per_step 0 n) |={∅}=> ⌜φ⌝)%I
     with "[-]" as "H"; last first.
@@ -235,20 +234,16 @@ Proof.
   { by rewrite big_sepL2_replicate_r // big_sepL_omap. }
   (* we run the adequacy proof again to get this assumption *)
   iPureIntro. intros e2 -> Hel.
-  eapply (wp_progress_gen use_credits);
+  eapply (wp_progress_gen hlc);
     [ done | clear stateI Φ fork_post state_interp_mono Hlen1 Hlen3 | done|done].
-  iIntros (??).
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
+  iIntros (?).
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iModIntro. iExists _, _, _, _. iFrame.
 Qed.
 
-(** Adequacy when using later credits *)
-Definition wp_strong_adequacy_lc := wp_strong_adequacy_gen true.
-Global Arguments wp_strong_adequacy_lc _ _ {_}.
-(** Adequacy when using no later credits *)
-Definition wp_strong_adequacy_no_lc := wp_strong_adequacy_gen false.
-Global Arguments wp_strong_adequacy_no_lc _ _ {_}.
-
+(** Adequacy when using later credits (the default) *)
+Definition wp_strong_adequacy := wp_strong_adequacy_gen HasLc.
+Global Arguments wp_strong_adequacy _ _ {_}.
 
 (** Since the full adequacy statement is quite a mouthful, we prove some more
 intuitive and simpler corollaries. These lemmas are morover stated in terms of
@@ -303,21 +298,21 @@ of laters per step must be 0, and the proof of [state_interp_mono] must have
 this specific proof term.
 *)
 (** Again, we first prove a lemma generic over the usage of credits. *)
-Lemma wp_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e σ φ :
-  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
+Lemma wp_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s e σ φ :
+  (∀ `{Hinv : !invGS_gen hlc Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisGS Λ Σ :=
-           IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
+       let _ : irisGS_gen hlc Λ Σ :=
+           IrisG Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
                  (λ _ _ _ _, fupd_intro _ _)
        in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy_gen use_credits Σ _); [ | done]=> ??.
-  iMod Hwp as (stateI fork_post) "[Hσ Hwp]"; first done.
+  eapply (wp_strong_adequacy_gen hlc Σ _); [ | done]=> ?.
+  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
   iExists (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
@@ -327,19 +322,15 @@ Proof.
 Qed.
 
 (** Instance for using credits *)
-Definition wp_adequacy_lc := wp_adequacy_gen true.
-Global Arguments wp_adequacy_lc _ _ {_}.
-(** Instance for no credits  *)
-Definition wp_adequacy_no_lc := wp_adequacy_gen false.
-Global Arguments wp_adequacy_no_lc _ _ {_}.
-
+Definition wp_adequacy := wp_adequacy_gen HasLc.
+Global Arguments wp_adequacy _ _ {_}.
 
-Lemma wp_invariance_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
-  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
+Lemma wp_invariance_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
+  (∀ `{Hinv : !invGS_gen hlc Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisGS Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
+       let _ : irisGS_gen hlc Λ Σ := IrisG Hinv (λ σ _, stateI σ) fork_post
               (λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
        stateI σ1 κs 0 ∗ WP e1 @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝)) →
@@ -347,8 +338,8 @@ Lemma wp_invariance_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e1 σ1 t2 
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy_gen use_credits Σ); [done| |done]=> ? Hc.
-  iMod (Hwp _ Hc κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
+  eapply (wp_strong_adequacy_gen hlc Σ); [done| |done]=> ?.
+  iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
   iExists (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
   iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
@@ -357,7 +348,5 @@ Proof.
   by iApply fupd_mask_intro_discard; first set_solver.
 Qed.
 
-Definition wp_invariance_lc := wp_invariance_gen true.
-Global Arguments wp_invariance_lc _ _ {_}.
-Definition wp_invariance_no_lc := wp_invariance_gen false.
-Global Arguments wp_invariance_no_lc _ _ {_}.
+Definition wp_invariance := wp_invariance_gen HasLc.
+Global Arguments wp_invariance _ _ {_}.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 9a651a70bb7537be385cf75eab8701121d36459d..311c9b6fc67b2877a6a0f5c91f1f5b04db7b9352 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
 example where we want it to be anything else. *)
-Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
+Definition atomic_wp `{!irisGS_gen hlc Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
   (E : coPset) (* *implementation* mask *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
@@ -83,7 +83,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
 
 (** Theory *)
 Section lemmas.
-  Context `{!irisGS Λ Σ} {TA TB : tele}.
+  Context `{!irisGS_gen hlc Λ Σ} {TA TB : tele}.
   Notation iProp := (iProp Σ).
   Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
 
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 5c78293c0dbe2e8057672405d0d539684414673e..b69c91816dceabf51c1aebcebad54539d5a86b6f 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.prelude Require Import options.
 
 Section wp.
-Context {Λ : ectxLanguage} `{!irisGS Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisGS_gen hlc Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index f90f71e20ed34e5651572e4468e8933cc922bf9e..522fab8b6af1a661fc0a541e216c3a21e2b52339 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -6,7 +6,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 
 Section lifting.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen hlc Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 22d9b2791518efb3c54b34a4ae85ce20d8b9d47b..267d8db8d4cc5e654e0d64abe9199d696f667445 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -51,11 +51,11 @@ Global Instance: Params (@ownP) 3 := {}.
 
 (* Adequacy *)
 Theorem ownP_adequacy Σ `{!ownPGpreS Λ Σ} s e σ φ :
-  (∀ `{!ownPGS Λ Σ, !HasLc Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{!ownPGS Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
-  intros Hwp. apply (wp_adequacy_lc Σ _).
-  iIntros (? ? κs).
+  intros Hwp. apply (wp_adequacy Σ _).
+  iIntros (? κs).
   iMod (own_alloc (●E σ ⋅ ◯E σ)) as (γσ) "[Hσ Hσf]";
     first by apply excl_auth_valid.
   iModIntro. iExists (λ σ κs, own γσ (●E σ))%I, (λ _, True%I).
@@ -64,14 +64,14 @@ Proof.
 Qed.
 
 Theorem ownP_invariance Σ `{!ownPGpreS Λ Σ} s e σ1 t2 σ2 φ :
-  (∀ `{!ownPGS Λ Σ, !HasLc Σ},
+  (∀ `{!ownPGS Λ Σ},
       ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
       |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance_lc Σ Λ s e σ1 t2 σ2 _)=> //.
-  iIntros (? ? κs).
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
+  iIntros (? κs).
   iMod (own_alloc (●E σ1 ⋅ ◯E σ1)) as (γσ) "[Hσ Hσf]";
     first by apply auth_both_valid_discrete.
   iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 8a509442d9242575ca4fe5baf1fce7455f06c116..6e295a13067ebd50d6dbbfdea57f4fda0e49d881 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Section adequacy.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen HasNoLc Λ Σ}.
 Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
@@ -104,7 +104,7 @@ Proof.
   iApply (twptp_app [_] with "(IH' [//])"). by iApply "IH".
 Qed.
 
-Lemma twptp_total `{!HasNoLc Σ} σ ns nt t :
+Lemma twptp_total σ ns nt t :
   state_interp σ ns [] nt -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
   iIntros "Hσ Ht". iRevert (σ ns nt) "Hσ". iRevert (t) "Ht".
@@ -117,7 +117,7 @@ Qed.
 End adequacy.
 
 Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
-  (∀ `{Hinv : !invGS Σ} `{!HasNoLc Σ},
+  (∀ `{Hinv : !invGS_gen HasNoLc Σ},
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (** We abstract over any instance of [irisG], and thus any value of
@@ -127,16 +127,16 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
          (num_laters_per_step : nat → nat)
          (fork_post : val Λ → iProp Σ)
          state_interp_mono,
-       let _ : irisGS Λ Σ :=
-           IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono
+       let _ : irisGS_gen HasNoLc Λ Σ :=
+           IrisG Hinv stateI fork_post num_laters_per_step state_interp_mono
        in
        stateI σ n [] 0 ∗ WP e @ s; ⊤ [{ Φ }]) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv HNC. iIntros "_".
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
-  set (iG := IrisG _ _ Hinv stateI fork_post num_laters_per_step stateI_mono).
-  iApply (@twptp_total _ _ iG _ _ n with "Hσ").
-  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv _ fork_post _ _)).
+  set (iG := IrisG Hinv stateI fork_post num_laters_per_step stateI_mono).
+  iApply (@twptp_total _ _ iG _ n with "Hσ").
+  by iApply (@twp_twptp _ _ (IrisG Hinv _ fork_post _ _)).
 Qed.
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 76fb2ff1c75f8f5145d76bb7c01b16a2a631501f..b5f21f96224d849f3b9c1f7fb5fcc655211204f0 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ectx_language total_weakestpre total_lift
 From iris.prelude Require Import options.
 
 Section wp.
-Context {Λ : ectxLanguage} `{!irisGS Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisGS_gen hlc Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index c2a1214ac5b79cfd0c717e19081778cb6870db53..8502c624029808732fb62e2bff4e2e3dfac71457 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export total_weakestpre.
 From iris.prelude Require Import options.
 
 Section lifting.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen hlc Λ Σ}.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index d71dfb12ae0e911c5d8e26d0ef893b1054345fed..b9ea90171d274cf9d7428eb49bfe56a328dccae6 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -8,7 +8,7 @@ Import uPred.
 definition of normal (i.e. partial) weakest precondition, with the exception
 that there is no later modality. Hence, instead of taking a Banach's fixpoint,
 we take a least fixpoint. *)
-Definition twp_pre `{!irisGS Λ Σ} (s : stuckness)
+Definition twp_pre `{!irisGS_gen hlc Λ Σ} (s : stuckness)
       (wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
@@ -25,7 +25,7 @@ Definition twp_pre `{!irisGS Λ Σ} (s : stuckness)
 
 (** This is some uninteresting bookkeeping to prove that [twp_pre_mono] is
 monotone. The actual least fixpoint [twp_def] can be found below. *)
-Local Lemma twp_pre_mono `{!irisGS Λ Σ} s
+Local Lemma twp_pre_mono `{!irisGS_gen hlc Λ Σ} s
     (wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
   ⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
     ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ.
@@ -42,12 +42,12 @@ Proof.
 Qed.
 
 (* Uncurry [twp_pre] and equip its type with an OFE structure *)
-Local Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
+Local Definition twp_pre' `{!irisGS_gen hlc Λ Σ} (s : stuckness) :
   (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
   prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
     uncurry3 ∘ twp_pre s ∘ curry3.
 
-Local Instance twp_pre_mono' `{!irisGS Λ Σ} s : BiMonoPred (twp_pre' s).
+Local Instance twp_pre_mono' `{!irisGS_gen hlc Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
   - iIntros (wp1 wp2 ??) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
@@ -57,17 +57,17 @@ Proof.
     rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Local Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
+Local Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Local Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
-Global Arguments twp' {Λ Σ _}.
+Global Arguments twp' {hlc Λ Σ _}.
 Global Existing Instance twp'.
-Local Lemma twp_unseal `{!irisGS Λ Σ} : twp = @twp_def Λ Σ _.
+Local Lemma twp_unseal `{!irisGS_gen hlc Λ Σ} : twp = @twp_def hlc Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
 Section twp.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen hlc Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -276,7 +276,7 @@ End twp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{!irisGS Λ Σ}.
+  Context `{!irisGS_gen hlc Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types v : val Λ.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 3119a20cf7c488f780fe459efeeedaaa854ea428..fc12397c1080cdd411ce51c1c15dd0c7302ef410 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -7,8 +7,8 @@ From iris.bi Require Export weakestpre.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invGS :> invGS Σ;
+Class irisGS_gen (hlc : has_lc) (Λ : language) (Σ : gFunctors) := IrisG {
+  iris_invGS :> invGS_gen hlc Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [Λstate] is the global state,
@@ -46,6 +46,9 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
     state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
 }.
 Global Opaque iris_invGS.
+Global Arguments IrisG {hlc Λ Σ}.
+
+Notation irisGS := (irisGS_gen HasLc).
 
 (** The predicate we take the fixpoint of in order to define the WP. *)
 (** In the step case, we both provide [S (num_laters_per_step ns)]
@@ -60,7 +63,7 @@ Global Opaque iris_invGS.
     can only be used by exactly one client.
   - The step-taking update can even be used by clients that opt out of
     later credits, e.g. because they use [BiFUpdPlainly]. *)
-Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
+Definition wp_pre `{!irisGS_gen hlc Λ Σ} (s : stuckness)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
@@ -76,7 +79,7 @@ Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
-Local Instance wp_pre_contractive `{!irisGS Λ Σ} s : Contractive (wp_pre s).
+Local Instance wp_pre_contractive `{!irisGS_gen hlc Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
   do 25 (f_contractive || f_equiv).
@@ -87,17 +90,17 @@ Proof.
   - by rewrite -IH.
 Qed.
 
-Local Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
+Local Definition wp_def `{!irisGS_gen hlc Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Local Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
-Global Arguments wp' {Λ Σ _}.
+Global Arguments wp' {hlc Λ Σ _}.
 Global Existing Instance wp'.
-Local Lemma wp_unseal `{!irisGS Λ Σ} : wp = @wp_def Λ Σ _.
+Local Lemma wp_unseal `{!irisGS_gen hlc Λ Σ} : wp = @wp_def hlc Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
-Context `{!irisGS Λ Σ}.
+Context `{!irisGS_gen hlc Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -415,7 +418,7 @@ End wp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{!irisGS Λ Σ}.
+  Context `{!irisGS_gen hlc Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types v : val Λ.
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index f14ffa9f95ee1caa17ea36974c803f8bd3fb698f..34ace6793daa9c77172f64434835eeab20441ee6 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -25,18 +25,18 @@ with a non-constant step index function. We thus use the more general
 [wp_adequacy], and it hence would make sense to see if we can prove a version
 of [wp_adequacy] for a non-constant step version. *)
 Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
-  (∀ `{!heapGS Σ, !HasLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp.
   apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy_lc Σ _); [|done].
-  iIntros (Hinv HC).
+  eapply (wp_strong_adequacy Σ _); [|done].
+  iIntros (Hinv).
   iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iMod (mono_nat_own_alloc) as (γ) "[Hsteps _]".
-  iDestruct (Hwp (HeapGS _ _ _ _ _ _ _) with "Hi") as "Hwp".
+  iDestruct (Hwp (HeapGS _ _ _ _ _ _ _ _) with "Hi") as "Hwp".
   iModIntro.
   iExists (λ σ ns κs nt, (gen_heap_interp σ.(heap) ∗
                           proph_map_interp κs σ.(used_proph_id) ∗
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 93725bafb7a878c79051873318e1ce85cbd5ec69..fe78ae541f4a7e3691e935f58c8c789812f22602 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -14,7 +14,7 @@ From iris.prelude Require Import options.
 (** The [array] connective is a version of [mapsto] that works
 with lists of values. *)
 
-Definition array `{!heapGS Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
+Definition array `{!heapGS_gen hlc Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   [∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v.
 
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
@@ -33,7 +33,7 @@ Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
 lead to overlapping instances. *)
 
 Section lifting.
-Context `{!heapGS Σ}.
+Context `{!heapGS_gen hlc Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types σ : state.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index ec22b73ed96fc7e8a77702ea0050e3349df8e282..15f88e961ac3117d4880c0a6b39184e7dac651c9 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -50,7 +50,7 @@ Definition array_init : val :=
     "src".
 
 Section proof.
-  Context `{!heapGS Σ}.
+  Context `{!heapGS_gen hlc Σ}.
 
   Lemma twp_array_free s E l vs (n : Z) :
     n = length vs →
diff --git a/iris_heap_lang/lib/assert.v b/iris_heap_lang/lib/assert.v
index 58dbd164a3fb64cf964d8ef3bc19a3d47f4f8b9a..4da507789521047ef972a09fdf3eeecdabe62e3e 100644
--- a/iris_heap_lang/lib/assert.v
+++ b/iris_heap_lang/lib/assert.v
@@ -10,7 +10,7 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
 Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.
 
-Lemma twp_assert `{!heapGS Σ} E (Φ : val → iProp Σ) e :
+Lemma twp_assert `{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
   WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
   WP (assert: e)%V @ E [{ Φ }].
 Proof.
@@ -18,7 +18,7 @@ Proof.
   wp_smart_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
-Lemma wp_assert `{!heapGS Σ} E (Φ : val → iProp Σ) e :
+Lemma wp_assert `{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
   WP (assert: e)%V @ E {{ Φ }}.
 Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 799b58df38d7a2b8b666b7e72ffd9597d18f6472..91fd17a56de34eba228c2bec495c94e13ec9a1c1 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -11,8 +11,8 @@ From iris.heap_lang Require Export class_instances.
 From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
 
-Class heapGS Σ := HeapGS {
-  heapGS_invGS : invGS Σ;
+Class heapGS_gen hlc Σ := HeapGS {
+  heapGS_invGS : invGS_gen hlc Σ;
   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) Σ;
@@ -21,8 +21,10 @@ Class heapGS Σ := HeapGS {
 }.
 Local Existing Instance heapGS_step_cnt.
 
+Notation heapGS := (heapGS_gen HasLc).
+
 Section steps.
-  Context `{!heapGS Σ}.
+  Context `{!heapGS_gen hlc Σ}.
 
   Local Definition steps_auth (n : nat) : iProp Σ :=
     mono_nat_auth_own heapGS_step_name 1 n.
@@ -58,7 +60,7 @@ Section steps.
 
 End steps.
 
-Global Program Instance heapGS_irisGS `{heapGS Σ} : irisGS heap_lang Σ := {
+Global Program Instance heapGS_irisGS `{!heapGS_gen hlc Σ} : irisGS_gen hlc heap_lang Σ := {
   iris_invGS := heapGS_invGS;
   state_interp σ step_cnt κs _ :=
     (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id) ∗
@@ -67,7 +69,7 @@ Global Program Instance heapGS_irisGS `{heapGS Σ} : irisGS heap_lang Σ := {
   num_laters_per_step n := n;
 }.
 Next Obligation.
-  iIntros (?? σ ns κs nt)  "/= ($ & $ & H)".
+  iIntros (??? σ ns κs nt)  "/= ($ & $ & H)".
   by iMod (steps_auth_update_S with "H") as "$".
 Qed.
 
@@ -88,7 +90,7 @@ Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V)
 make setoid rewriting in the predicate [I] work we need actual definitions
 here. *)
 Section definitions.
-  Context `{!heapGS Σ}.
+  Context `{!heapGS_gen hlc Σ}.
   Definition inv_mapsto_own (l : loc) (v : val) (I : val → Prop) : iProp Σ :=
     inv_mapsto_own l (Some v) (from_option I False).
   Definition inv_mapsto (l : loc) (I : val → Prop) : iProp Σ :=
@@ -105,7 +107,7 @@ Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
 Section lifting.
-Context `{!heapGS Σ}.
+Context `{!heapGS_gen hlc Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val → iProp Σ.
 Implicit Types efs : list expr.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index a77de67b67511395d43e28b09986c8a91ab86fac..49f45e643586c793e87563127c134d671c23b3d9 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -6,11 +6,11 @@ From iris.heap_lang Require Import notation.
 From iris.prelude Require Import options.
 Import uPred.
 
-Lemma tac_wp_expr_eval `{!heapGS Σ} Δ s E Φ e e' :
+Lemma tac_wp_expr_eval `{!heapGS_gen hlc Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
-Lemma tac_twp_expr_eval `{!heapGS Σ} Δ s E Φ e e' :
+Lemma tac_twp_expr_eval `{!heapGS_gen hlc Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
@@ -28,7 +28,7 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
   end.
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
-Lemma tac_wp_pure `{!heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapGS_gen hlc Σ} Δ Δ' s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -41,7 +41,7 @@ Proof.
   rewrite HΔ' -lifting.wp_pure_step_later //.
   iIntros "Hwp !> _" => //.
 Qed.
-Lemma tac_twp_pure `{!heapGS Σ} Δ s E K e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapGS_gen hlc Σ} Δ s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
@@ -53,17 +53,17 @@ Proof.
   rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
+Lemma tac_wp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
+Lemma tac_twp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_unseal=> ->. by apply twp_value. Qed.
 
-Lemma tac_wp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
+Lemma tac_wp_value `{!heapGS_gen hlc Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_unseal=> ->. by rewrite wp_value_fupd. Qed.
-Lemma tac_twp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
+Lemma tac_twp_value `{!heapGS_gen hlc Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_unseal=> ->. by rewrite twp_value_fupd. Qed.
 
@@ -171,12 +171,12 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
 Tactic Notation "wp_pair" := wp_pure (Pair _ _).
 Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
 
-Lemma tac_wp_bind `{!heapGS Σ} K Δ s E Φ e f :
+Lemma tac_wp_bind `{!heapGS_gen hlc Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
-Lemma tac_twp_bind `{!heapGS Σ} K Δ s E Φ e f :
+Lemma tac_twp_bind `{!heapGS_gen hlc Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
   envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
@@ -207,7 +207,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
 
 (** Heap tactics *)
 Section heap.
-Context `{!heapGS Σ}.
+Context `{!heapGS_gen hlc Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/iris_heap_lang/total_adequacy.v b/iris_heap_lang/total_adequacy.v
index a6287612f45aea9f7e6c5315e5ca91dfade07b1c..fb06eb47dde088210d549d4106af65be30626d27 100644
--- a/iris_heap_lang/total_adequacy.v
+++ b/iris_heap_lang/total_adequacy.v
@@ -6,10 +6,10 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 Definition heap_total Σ `{!heapGpreS Σ} s e σ φ :
-  (∀ `{!heapGS Σ, !HasNoLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
+  (∀ `{!heapGS_gen HasNoLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
   sn erased_step ([e], σ).
 Proof.
-  intros Hwp; eapply (twp_total _ _); iIntros (??) "".
+  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
   iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
@@ -20,5 +20,5 @@ Proof.
                    proph_map_interp κs σ.(used_proph_id) ∗
                    mono_nat_auth_own γ 1 ns)%I),
     id, (λ _, True%I), _; iFrame.
-  by iApply (Hwp (HeapGS _ _ _ _ _ _ _)).
+  by iApply (Hwp (HeapGS _ _ _ _ _ _ _ _)).
 Qed.
diff --git a/tests/algebra.v b/tests/algebra.v
index 68cc8177c0e436362083a7f2902bbf0778c7b62c..8ec25e7b301d4a37e4577f17d3b7808aa72c6e74 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -27,7 +27,7 @@ Proof. reflexivity. Qed.
 Global Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
 
 Section tests.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
     λne P v, (▷ (P v))%I.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 2c9207a87581dd4baa63467d40d87730fa22a6ed..2ca1c26e84f2b2fdee24b0bd5de1776c38a44b5e 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -170,13 +170,13 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapGS0 : heapGS Σ
+  heapGS0 : heapGS_gen HasLc Σ
   ============================
   @bi_emp_valid (uPredI (iResUR Σ))
     (@fupd (bi_car (uPredI (iResUR Σ)))
        (@bi_fupd_fupd (uPredI (iResUR Σ))
-          (@uPred_bi_fupd Σ
-             (@iris_invGS heap_lang Σ (@heapGS_irisGS Σ heapGS0))))
+          (@uPred_bi_fupd HasLc Σ
+             (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)
        (@bi_pure (uPredI (iResUR Σ)) True))
 1 goal
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 8e5fc551a96ca1415bd51d8907b847eeed58e7b8..2bb43ba85990ec66f626bcf1ac13f33250789719 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -452,11 +452,11 @@ End error_tests.
 
 (* Test a closed proof *)
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
-Proof. eapply (heap_adequacy heapΣ)=> ??. iIntros "_". by iApply heap_e_spec. Qed.
+Proof. eapply (heap_adequacy heapΣ). iIntros (?) "_". by iApply heap_e_spec. Qed.
 
 Lemma heap_e_totally_adequate σ : sn erased_step ([heap_e], σ).
 Proof.
-  eapply (heap_total heapΣ NotStuck _ _ (const True))=> ??. iIntros "_".
-  rewrite /heap_e /=.
+  eapply (heap_total heapΣ NotStuck _ _ (const True)).
+  iIntros (?) "_". rewrite /heap_e /=.
   wp_alloc l. wp_load. wp_store. wp_load. auto.
 Qed.
diff --git a/tests/iris_notation.v b/tests/iris_notation.v
index 735ef8d0b4da5e72e17fe647b081abb84875a6c1..29f77c3e10431708ae30e8f1e5da48f6fcd3e6ad 100644
--- a/tests/iris_notation.v
+++ b/tests/iris_notation.v
@@ -24,7 +24,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
   Implicit Types P Q R : iProp Σ.
 
   (* Test scopes for bupd and fupd *)
diff --git a/tests/one_shot.v b/tests/one_shot.v
index f6aa093dc229f640bad8b4a38b2dc905e50fc7d6..378177ec1cac857a5ec8462674ea08494500dc5e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -135,7 +135,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ??. iIntros "_". iApply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
 
 (* Since we check the output of the test files, this means
 our test suite will fail if we ever accidentally add an axiom
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index b9ca8654bbe231657246b32f491d3d19b96dc61c..506ac4cc71f5ec82f54c09325872fd89242f8e7b 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -153,4 +153,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ??. iIntros "_". iApply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index 5db0de8ae8ce60a59390d6b2544f32df7b9f11ac..a76fddef9bf93f9f26e53c21e501a7ca70292ddc 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -1,7 +1,8 @@
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -13,8 +14,9 @@
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -28,8 +30,9 @@
   |={⊤ ∖ ↑N,⊤}=> ▷ P
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -45,8 +48,9 @@
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -63,8 +67,9 @@
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -83,8 +88,9 @@
     (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -113,8 +119,9 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -128,8 +135,9 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index f7f4d6021b582916b3a3b11f5e2dd84985c22bbc..4b950c2755ec4df75f4ff9842d07c53f9b02a818 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -58,7 +58,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invGS Σ, !cinvG Σ, !na_invG Σ}.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
@@ -236,7 +236,7 @@ Section iris_tests.
 End iris_tests.
 
 Section monpred_tests.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
   Context {I : biIndex}.
   Local Notation monPred := (monPred I (iPropI Σ)).
   Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 229402b79781bad7359cb55b0a906ed47c778181..11b3aa04200312c452783759cd29312ff03b4ac4 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,7 +1,8 @@
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -13,8 +14,9 @@
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -28,8 +30,9 @@
   |={⊤ ∖ ↑N,⊤}=> ▷ P
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -40,8 +43,9 @@
   cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -59,8 +63,9 @@
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -79,8 +84,9 @@
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -101,8 +107,9 @@
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -115,8 +122,9 @@
     na_own t E1 ∗ na_own t E2 ∗ ▷ P
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -145,8 +153,9 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -158,8 +167,9 @@ Tactic failure: iInv: invariant "H2" not found.
   own γ 1%Qp
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -176,8 +186,9 @@ Tactic failure: iMod: "H" not fresh.
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   n, m : nat
@@ -190,8 +201,9 @@ Tactic failure: iMod: "H" not fresh.
      : string
 2 goals
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   n, m : nat
@@ -208,8 +220,9 @@ goal 2 is:
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -223,8 +236,9 @@ goal 2 is:
      : string
 1 goal
   
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 6884d140b88d0bafda214683ea802b88430cbabc..b6bbbdb2d8ca99ec367a3ce8438eb6fca5ec53cf 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -53,7 +53,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invGS Σ, !cinvG Σ, !na_invG Σ}.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
@@ -262,7 +262,7 @@ Section iris_tests.
 End iris_tests.
 
 Section monpred_tests.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
   Context {I : biIndex}.
   Local Notation monPred := (monPred I (iPropI Σ)).
   Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 37fde33a6b980db77a5656a3982692601d2a531b..aceb32e69da757e4fee8ae646550171d93f3013b 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -57,8 +57,9 @@ Tactic failure: iFrame: cannot frame (P i).
 1 goal
   
   I : biIndex
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   N : namespace
   𝓟 : iProp Σ
   ============================
@@ -69,8 +70,9 @@ Tactic failure: iFrame: cannot frame (P i).
 1 goal
   
   I : biIndex
+  hlc : has_lc
   Σ : gFunctors
-  invGS0 : invGS Σ
+  invGS_gen0 : invGS_gen hlc Σ
   N : namespace
   𝓟 : iProp Σ
   ============================
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 25b7fe1977c75c6e75cf4e4be9710e1ef9991f70..638add08ebd83ffded99a1b0dc59f845467ea583 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -180,7 +180,7 @@ Section tests.
 End tests.
 
 Section tests_iprop.
-  Context {I : biIndex} `{!invGS Σ}.
+  Context {I : biIndex} `{!invGS_gen hlc Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
   Implicit Types P Q R : monPred.