diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd1cf310a361fb73cb2426d1096d47c58aee3f17..2482b3d14e3c91f32e1e6ed1f85b896dc86fbd95 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -152,7 +152,7 @@ Coq 8.13 is no longer supported.
   `iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre)
 * Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over
   lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See
-  [iris/proofmode/base.v](proofmode/base.v) for documentation on how
+  [proofmode/base.v](iris/proofmode/base.v) for documentation on how
   to use these tactics to convert your own fixed arity tactics to an n-ary
   variant.
 
@@ -181,6 +181,10 @@ Coq 8.13 is no longer supported.
 * Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
 * Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim)
+* Make the generic `lock` specification a typeclass. Code that is generic about
+  lock implementations, or that instantiates that specification, needs
+  adjustment. See [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for
+  documentation on how to work with this specification.
 
 **LaTeX changes:**
 
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 0ecf54c5513173efdbdb0a6a6eee4d86c53c701a..5c66f9c7c283d4d1c6647cade4a331233811f3d6 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -1,28 +1,37 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Import primitive_laws notation.
+From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 (** 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 {
+[heapGS_gen] in scope that could possibly apply.
+
+Only one instance of this class should ever be in scope. To write a library that
+is generic over the lock, just add a [`{lock}] implicit parameter. To use a
+particular lock instance, use [Local Existing Instance <lock instance>].
+
+When writing an instance of this class, please take care not to shadow the class
+projections (e.g., either use [Local Definition newlock] or avoid the name
+[newlock] altogether), and do not register an instance -- just make it a
+[Definition] that others can register later. *)
+Class lock `{!heapGS_gen hlc Σ} := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
   release : val;
   (** * Predicates *)
   (** [name] is used to associate locked with [is_lock] *)
-  name : Type;
+  lock_name : Type;
   (** No namespace [N] parameter because we only expose program specs, which
   anyway have the full mask. *)
-  is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
-  locked (γ: name) : iProp Σ;
+  is_lock (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
+  locked (γ: lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_lock_ne γ lk : Contractive (is_lock γ lk);
-  is_lock_persistent γ lk R : Persistent (is_lock γ lk R);
+  is_lock_persistent γ lk R :> Persistent (is_lock γ lk R);
   is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2;
-  locked_timeless γ : Timeless (locked γ);
+    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2;
+  locked_timeless γ :> Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (** * Program specs *)
   newlock_spec (R : iProp Σ) :
@@ -34,7 +43,14 @@ Structure lock `{!heapGS_gen hlc Σ} := Lock {
 }.
 Global Hint Mode lock + + + : typeclass_instances.
 
-Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
+Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock} γ lk :
+  Contractive (is_lock γ lk).
+Proof.
+  apply (uPred.contractive_internal_eq (M:=iResUR Σ)).
+  iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>".
+  iSplit; iIntros "H"; iApply (is_lock_iff with "H");
+    iNext; iRewrite "HPQ"; auto.
+Qed.
 
-Global Instance is_lock_proper hlc Σ `{!heapGS_gen hlc Σ} (L : lock) γ lk :
-  Proper ((≡) ==> (≡)) (L.(is_lock) γ lk) := ne_proper _.
+Global Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock} γ lk :
+  Proper ((≡) ==> (≡)) (is_lock γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 6daea74fa2195345a9ff642346e2f65d984175c2..e2cddb9ee597d2d1815449c9bd4d4814c0c96893 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -25,20 +25,20 @@ Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section tada.
-  Context `{!heapGS Σ, !lockG Σ} (l : lock).
+  Context `{!heapGS Σ, !lockG Σ, !lock}.
 
   Record tada_lock_name := TadaLockName {
     tada_lock_name_state : gname;
-    tada_lock_name_lock : l.(name);
+    tada_lock_name_lock : lock_name;
   }.
   
   Definition tada_lock_state (γ : tada_lock_name) (s : state) : iProp Σ :=
     ghost_var γ.(tada_lock_name_state) (3/4) s ∗
     if s is Locked then
-      l.(locked) γ.(tada_lock_name_lock) ∗ ghost_var γ.(tada_lock_name_state) (1/4) Locked
+      locked γ.(tada_lock_name_lock) ∗ ghost_var γ.(tada_lock_name_state) (1/4) Locked
     else True.
   Definition tada_is_lock (γ : tada_lock_name) (lk : val) : iProp Σ :=
-    l.(is_lock) γ.(tada_lock_name_lock) lk
+    is_lock γ.(tada_lock_name_lock) lk
       (ghost_var γ.(tada_lock_name_state) (1/4) Free).
 
   Global Instance tada_is_lock_persistent γ lk : Persistent (tada_is_lock γ lk).
@@ -56,7 +56,7 @@ Section tada.
 
   Lemma newlock_tada_spec :
     {{{ True }}}
-      l.(newlock) #()
+      newlock #()
     {{{ lk γ, RET lk; tada_is_lock γ lk ∗ tada_lock_state γ Free }}}.
   Proof.
     iIntros (Φ) "_ HΦ".
@@ -64,7 +64,7 @@ Section tada.
     replace 1%Qp with (3/4 + 1/4)%Qp; last first.
     { rewrite Qp.three_quarter_quarter //. }
     iDestruct "Hvar" as "[Hvar1 Hvar2]".
-    wp_apply (l.(newlock_spec) with "Hvar2") as (lk γlock) "Hlock".
+    wp_apply (newlock_spec with "Hvar2") as (lk γlock) "Hlock".
     iApply ("HΦ" $! lk (TadaLockName _ _)).
     iFrame.
   Qed.
@@ -72,11 +72,11 @@ Section tada.
   Lemma acquire_tada_spec γ lk :
     tada_is_lock γ lk -∗
     <<< ∀∀ s, tada_lock_state γ s >>>
-      l.(acquire) lk @ ∅
+      acquire lk @ ∅
     <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked, RET #() >>>.
   Proof.
     iIntros "#Hislock %Φ AU". iApply wp_fupd.
-    wp_apply (l.(acquire_spec) with "Hislock") as "[Hlocked Hvar1]".
+    wp_apply (acquire_spec with "Hislock") as "[Hlocked Hvar1]".
     iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
     iCombine "Hvar1 Hvar2" gives %[_ <-].
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
@@ -87,7 +87,7 @@ Section tada.
   Lemma release_tada_spec γ lk :
     tada_is_lock γ lk -∗
     <<< tada_lock_state γ Locked >>>
-      l.(release) lk @ ∅
+      release lk @ ∅
     <<< tada_lock_state γ Free, RET #() >>>.
   Proof.
     iIntros "#Hislock %Φ AU". iApply fupd_wp.
@@ -95,7 +95,7 @@ Section tada.
     iMod (ghost_var_update_2 Free with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
     { rewrite Qp.three_quarter_quarter //. }
     iMod ("Hclose" with "[$Hvar1]"). iModIntro.
-    wp_apply (l.(release_spec) with "[$Hislock $Hlocked $Hvar2]").
+    wp_apply (release_spec with "[$Hislock $Hlocked $Hvar2]").
     auto.
   Qed.
 
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 5218861f67f12bacd01b328b58611ca4f89225a1..c449f45c6f4484e7e7d8f32a5b49bc66764b4c82 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -6,9 +6,9 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import lock.
 From iris.prelude Require Import options.
 
-Definition newlock : val := λ: <>, ref #false.
-Definition try_acquire : val := λ: "l", CAS "l" #false #true.
-Definition acquire : val :=
+Local Definition newlock : val := λ: <>, ref #false.
+Local Definition try_acquire : val := λ: "l", CAS "l" #false #true.
+Local Definition acquire : val :=
   rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
 Definition release : val := λ: "l", "l" <- #false.
 
@@ -26,30 +26,20 @@ Section proof.
   Context `{!heapGS_gen hlc Σ, !lockG Σ}.
   Let N := nroot .@ "spin_lock".
 
-  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
+  Local Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
     ∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R.
 
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+  Local Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     ∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R).
 
-  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
+  Local Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
 
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Local Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
 
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
-  Proof. solve_contractive. Qed.
-
   (** The main proofs. *)
-  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
-  Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
-  Proof. apply _. Qed.
-
-  Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Local Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2.
   Proof.
     iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
     iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
@@ -58,7 +48,7 @@ Section proof.
       first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
   Qed.
 
-  Lemma newlock_spec (R : iProp Σ):
+  Local Lemma newlock_spec (R : iProp Σ):
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite /newlock /=.
@@ -69,7 +59,7 @@ Section proof.
     iModIntro. iApply "HΦ". iExists l. eauto.
   Qed.
 
-  Lemma try_acquire_spec γ lk R :
+  Local Lemma try_acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} try_acquire lk
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
@@ -82,7 +72,7 @@ Section proof.
       rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
 
-  Lemma acquire_spec γ lk R :
+  Local Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
@@ -91,7 +81,7 @@ Section proof.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 
-  Lemma release_spec γ lk R :
+  Local Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
@@ -102,9 +92,7 @@ Section proof.
   Qed.
 End proof.
 
-Global Typeclasses Opaque is_lock locked.
-
-Canonical Structure spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
+Definition 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 0827bcd7d169db1154cc33c86009124dbee11de4..02c4e48d071cb9983206c99655b54317ebc2e52d 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -6,24 +6,24 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Export lock.
 From iris.prelude Require Import options.
 
-Definition wait_loop: val :=
+Local Definition wait_loop: val :=
   rec: "wait_loop" "x" "lk" :=
     let: "o" := !(Fst "lk") in
     if: "x" = "o"
       then #() (* my turn *)
       else "wait_loop" "x" "lk".
 
-Definition newlock : val :=
+Local Definition newlock : val :=
   λ: <>, ((* owner *) ref #0, (* next *) ref #0).
 
-Definition acquire : val :=
+Local Definition acquire : val :=
   rec: "acquire" "lk" :=
     let: "n" := !(Snd "lk") in
     if: CAS (Snd "lk") "n" ("n" + #1)
       then wait_loop "n" "lk"
       else "acquire" "lk".
 
-Definition release : val :=
+Local Definition release : val :=
   λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
 
 (** The CMRAs we need. *)
@@ -41,38 +41,29 @@ Section proof.
   Context `{!heapGS_gen hlc Σ, !tlockG Σ}.
   Let N := nroot .@ "ticket_lock".
 
-  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
+  Local Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
     ∃ o n : nat,
       lo ↦ #o ∗ ln ↦ #n ∗
       own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
       ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))).
 
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+  Local Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     ∃ lo ln : loc,
       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R).
 
-  Definition issued (γ : gname) (x : nat) : iProp Σ :=
+  Local Definition issued (γ : gname) (x : nat) : iProp Σ :=
     own γ (◯ (ε, GSet {[ x ]})).
 
-  Definition locked (γ : gname) : iProp Σ := ∃ o, own γ (◯ (Excl' o, GSet ∅)).
+  Local Definition locked (γ : gname) : iProp Σ := ∃ o, own γ (◯ (Excl' o, GSet ∅)).
 
-  Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_contractive γ lk : Contractive (is_lock γ lk).
-  Proof. solve_contractive. Qed.
-  Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
-  Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
-  Proof. apply _. Qed.
-
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Local Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
     iIntros "[%σ1 H1] [%σ2 H2]".
     iCombine "H1 H2" gives %[[] _]%auth_frag_op_valid_1.
   Qed.
 
-  Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Local Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2.
   Proof.
     iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
     iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
@@ -81,7 +72,7 @@ Section proof.
       (iDestruct "H" as "[[Hâ—¯ H]|Hâ—¯]"; [iLeft; iFrame "Hâ—¯"; by iApply "HR"|by iRight]).
   Qed.
 
-  Lemma newlock_spec (R : iProp Σ) :
+  Local Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". wp_lam.
@@ -94,7 +85,7 @@ Section proof.
     wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
-  Lemma wait_loop_spec γ lk x R :
+  Local Lemma wait_loop_spec γ lk x R :
     {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
     iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
@@ -115,7 +106,7 @@ Section proof.
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
   Qed.
 
-  Lemma acquire_spec γ lk R :
+  Local Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
     iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
@@ -144,7 +135,7 @@ Section proof.
       wp_pures. by iApply "IH"; auto.
   Qed.
 
-  Lemma release_spec γ lk R :
+  Local Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
@@ -172,9 +163,7 @@ Section proof.
   Qed.
 End proof.
 
-Global Typeclasses Opaque is_lock issued locked.
-
-Canonical Structure ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
+Definition 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/heap_lang.v b/tests/heap_lang.v
index 7f3f6270b15aa9e56386f2deb505146664019bf2..96d71b08ba31fb59e1cd40c36731cd0e72ff15a2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,8 +1,6 @@
 From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation.
-(* Import lang *again*. This used to break notation. *)
-From iris.heap_lang Require Import lang.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.lock.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -515,3 +513,28 @@ Proof.
   iIntros (?) "_". rewrite /heap_e /=.
   wp_alloc l. wp_load. wp_store. wp_load. auto.
 Qed.
+
+(** Just making sure the lock typeclass actually works. *)
+Section lock.
+  Context `{!heapGS Σ, !lock}.
+
+  Definition lock_client : val :=
+    λ: "loc" "lock",
+      acquire "lock";;
+      "loc" <- #42;;
+      release "lock".
+
+  Lemma wp_lock_client loc lock γ :
+    is_lock γ lock (∃ v, loc ↦ v) -∗
+    WP lock_client #loc lock {{ _, True }}.
+  Proof.
+    iIntros "#Hislock".
+    wp_lam. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    wp_store.
+    wp_smart_apply (release_spec with "[$Hlocked Hloc]").
+    { iFrame "Hislock". eauto. }
+    eauto.
+  Qed.
+
+End lock.
+