diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89bc4ab2323ce9d45f893b75db1ceee808c56dfc..a5783e424cbb3aa9ea307fd3e765bca3d91f0fd6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -71,14 +71,19 @@ lemma.
 * Prepare for supporting later credits, by adding a resource `£ n` describing
   ownership of `n` credits that can be eliminated at fancy updates.
   Note that HeapLang has not yet been equipped with support for later credits.
-  To retain backwards compatibility with the interaction laws of fancy updates
-  with the plainly modality (`BiFUpdPlainly`), which are incompatible with
-  later credits, the logic is parameterized by two typeclasses, `HasLc`
-  and `HasNoLc`, that allow opting for either later credits or `BiFUpdPlainly`.
-  The soundness lemmas for the fancy update modality are available in two versions,
-  with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
-  The lemmas without later credits still generate credits, but they cannot be used
-  in any meaningful way. The lemma `step_fupdN_soundness_gen` is generic over this choice.
+  + To retain backwards compatibility with the interaction laws of fancy updates
+    with the plainly modality (`BiFUpdPlainly`), which are incompatible with
+    later credits, the logic has a new parameter of type `has_lc`, which is
+    either `HasLc` or `HasNoLc`. The parameter is an index of the `invGS_gen`
+    typeclass; the old `invGS` is an alias for `invGS_gen HasLc` so that
+    developments default to having later credits available. Libraries that want
+    to be generic over whether credits are available or not, and proofs that
+    need `BiFUpdPlainly`, need to be changed to use `invGS_gen` rather than
+    `invGS`.
+  + The core soundness lemma `step_fupdN_soundness_gen` similarly takes a `has_lc`
+    parameter to control how the logic is supposed to be instantiated. The lemma
+    always generates credits, but they cannot be used in any meaningful way unless
+    `HasLc` is picked.
 * Add discardable fractions `dfrac` to `saved_anything_own`, `saved_prop_own`,
   and `saved_pred_own`, so they can be updated. The previous persistent versions
   can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
@@ -96,17 +101,16 @@ lemma.
   + All lifting lemmas have been altered to provide credits.
     `wp_lift_step_fupdN` provides `S (num_laters_per_step ns)` credits, while all other
     lemmas always provide one credit.
-* In line with the support for later credits (see `base_logic`), the adequacy statements
-  have been changed to account for `HasLc` and `HasNoLc`:
-  + The lemma `twp_total` (total adequacy) provides an additional assumption `HasNoLc`.
-    Clients of the adequacy proof will need to introduce this additional assumption and
-    keep it around in case `BiFUpdPlainly` is used.
+* In line with the support for later credits (see `base_logic`), `irisGS_gen`
+  now also has a `has_lc` parameter and the adequacy statements have been
+  changed to account for that:
+  + The lemma `twp_total` (total adequacy) provides `irisGS_gen HasNoLc`. Clients
+    of the adequacy proof will need to make sure to be either generic over the
+    choice of `has_lc` or explicitly opt-out of later credits.
   + The adequacy lemmas for the partial WP, in particular `wp_adequacy`,
-    `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors,
-    one providing `HasLc` to enable the use of later credits in the future (suffix `_lc`),
-    and one without support for later credits, providing `HasNoLc` (suffix `_no_lc`).
-    Clients of the adequacy proof will need to opt for either of these and introduce
-    the additional assumptions.
+    `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors:
+    the old names generate `irisGS` (a short-hand for `irisGS_gen HasLc`); new
+    lemmas with a `_gen` suffix leave the choice of `has_lc` to the user.
   + The parameter for the stuckness bit `s` in `wp_strong_adequacy{_lc, _no_lc}` has
     moved up and is now universally quantified in the lemma instead of being existentially
     quantified at the Iris-level. For clients that already previously quantified over `s`
@@ -120,14 +124,13 @@ lemma.
   number of steps taken so far. This number is tied to ghost state in the state
   interpretation, which is exposed, updated, and used with new lemmas
   `wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
-* In line with the support for later credits (see `base_logic`), the adequacy statements
-  for HeapLang have been changed:
-  + `heap_adequacy` provides the additional assumption `HasLc`, which needs to be
-    introduced by clients and will enable using new proof rules for later credits
-    in the future.
+* In line with the support for later credits (see `base_logic`), `heapGS_gen`
+  now takes an additional `has_lc` parameter, and `heapGS` is a short-hand for
+  `heapGS_gen HasLc`. The adequacy statements for HeapLang have been changed
+  accordingly:
+  + `heap_adequacy` provides `heapGS`, thus enabling the use of later credits.
     This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
-  + `heap_total` provides the additional assumption `HasNoLc`, which needs to be
-    introduced by clients and needs to be kept around to use the laws in `BiFUpdPlainly`.
+  + `heap_total` provides `heapGS_gen HasNoLc`.
   Currently, the primitive laws for HeapLang do not yet provide later credits.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
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/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 0bfa20012d259f429f2ef9ce2f5ce0f997cd448d..78c38cfc30ecc6a403261724d76460dc173f3bc7 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -5,8 +5,18 @@ From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import notation proofmode.
 From iris.prelude Require Import options.
 
-(** A general logically atomic interface for a heap. *)
-Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
+(** A general logically atomic interface for a heap.
+All parameters are implicit, since it is expected that there is only one
+[heapGS_gen] in scope that could possibly apply. For example:
+  
+  Context `{!heapGS_gen hlc Σ, !atomic_heap}.
+
+Or, for libraries that require later credits:
+
+  Context `{!heapGS Σ, !atomic_heap}.
+
+*)
+Class atomic_heap `{!heapGS_gen hlc Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   free : val;
@@ -45,7 +55,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
       <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
-Global Arguments atomic_heap _ {_}.
+Global Hint Mode atomic_heap + + + : typeclass_instances.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
@@ -69,7 +79,7 @@ Module notation.
 End notation.
 
 Section derived.
-  Context `{!heapGS Σ, !atomic_heap Σ}.
+  Context `{!heapGS_gen hlc Σ, !atomic_heap}.
 
   Import notation.
 
@@ -99,7 +109,7 @@ Definition primitive_cmpxchg : val :=
   λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
 
 Section proof.
-  Context `{!heapGS Σ}.
+  Context `{!heapGS_gen hlc Σ}.
 
   Lemma primitive_alloc_spec (v : val) :
     {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
@@ -148,7 +158,7 @@ End proof.
 
 (* NOT an instance because users should choose explicitly to use it
      (using [Explicit Instance]). *)
-Definition primitive_atomic_heap `{!heapGS Σ} : atomic_heap Σ :=
+Definition primitive_atomic_heap `{!heapGS_gen hlc Σ} : atomic_heap :=
   {| alloc_spec := primitive_alloc_spec;
      free_spec := primitive_free_spec;
      load_spec := primitive_load_spec;
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 9084375be27e0283aa83b0de124439c5c2fb52e3..5e8eb17ed415bfe6fc4a9acc2b7f6d6d855f2986 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -38,7 +38,7 @@ End increment_physical.
 (** Next: logically atomic increment on top of an arbitrary logically atomic heap *)
 
 Section increment.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ, !atomic_heap}.
 
   Import atomic_heap.notation.
 
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index a06b580b9714d50c61ac85b9d0f526328e8b656d..0ecf54c5513173efdbdb0a6a6eee4d86c53c701a 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -2,7 +2,10 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import primitive_laws notation.
 From iris.prelude Require Import options.
 
-Structure lock Σ `{!heapGS Σ} := Lock {
+(** A general interface for a lock.
+All parameters are implicit, since it is expected that there is only one
+[heapGS_gen] in scope that could possibly apply. *)
+Structure lock `{!heapGS_gen hlc Σ} := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
@@ -29,14 +32,9 @@ Structure lock Σ `{!heapGS Σ} := Lock {
   release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
-
-Global Arguments newlock {_ _} _.
-Global Arguments acquire {_ _} _.
-Global Arguments release {_ _} _.
-Global Arguments is_lock {_ _} _ _ _ _.
-Global Arguments locked {_ _} _ _.
+Global Hint Mode lock + + + : typeclass_instances.
 
 Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Global Instance is_lock_proper Σ `{!heapGS Σ} (L: lock Σ) γ lk:
-  Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
+Global Instance is_lock_proper hlc Σ `{!heapGS_gen hlc Σ} (L : lock) γ lk :
+  Proper ((≡) ==> (≡)) (L.(is_lock) γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/par.v b/iris_heap_lang/lib/par.v
index 1f9d69c1210b324cbadc2fc43176dccdbfeab8eb..9645118f96b2f76c0aaa641cebccc55f93038c55 100644
--- a/iris_heap_lang/lib/par.v
+++ b/iris_heap_lang/lib/par.v
@@ -15,7 +15,7 @@ Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
-Context `{!heapGS Σ, !spawnG Σ}.
+Context `{!heapGS_gen hlc Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been
    brought together.  That is strictly stronger than first stripping a later
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 70573628927101a2b11bd4b6f6c1a7f5c0a0e93f..20780846b7837cc8cfd9729179bfd2a111605b7f 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -29,7 +29,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!heapGS Σ, !spawnG Σ} (N : namespace).
+Context `{!heapGS_gen hlc Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 6b0ab568bf41dcbe1ce54f43b366fac7abbef558..f0fe1f9049b27ef4d7b0248fce0a1c89f1d51edf 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -23,7 +23,7 @@ Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS Σ, !lockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !lockG Σ}.
   Let N := nroot .@ "spin_lock".
 
   Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
@@ -104,7 +104,7 @@ End proof.
 
 Typeclasses Opaque is_lock locked.
 
-Canonical Structure spin_lock `{!heapGS Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index c52b35e3d6abfa88c18117c7370a33ae74a80d5e..ec8d4bdbc9ef804d9ddfacfc9b7d2520fbeec28a 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -38,7 +38,7 @@ Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS Σ, !tlockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !tlockG Σ}.
   Let N := nroot .@ "ticket_lock".
 
   Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
@@ -174,7 +174,7 @@ End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Canonical Structure ticket_lock `{!heapGS Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
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/atomic.ref b/tests/atomic.ref
index 0c7d1674c490a6b94777c96bcd2e76c136a1d8ad..177f9876e84679dc6d5f2d9a8504aa37e535dc64 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -4,7 +4,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   Q : iProp Σ
   l : loc
   v : val
@@ -20,7 +20,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   P : iProp Σ
   l : loc
   ============================
@@ -33,7 +33,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   P : iProp Σ
   l : loc
   ============================
diff --git a/tests/atomic.v b/tests/atomic.v
index 8fa7ac6fd3937b46b0229a0c937c03ebf69a8884..ee5264cfaf54afc46670ebcd3901dcd03c4612ec 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -27,7 +27,7 @@ Section general_bi_tests.
 End general_bi_tests.
 
 Section tests.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap}.
   Import atomic_heap.notation.
 
   (* FIXME: removing the `val` type annotation breaks printing. *)
@@ -41,7 +41,7 @@ End tests.
 
 (* Test if we get reasonable error messages with non-laterable assertions in the context. *)
 Section error.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap}.
   Import atomic_heap.notation.
 
   Check "non_laterable".
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.