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/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".