diff --git a/base_logic/lib/na_invariants.v b/base_logic/lib/na_invariants.v
index 508b88300b038e91ad2219c7ae5b43a557f9acff..e9084a60c592259f0aa41fd6c0063dedd267fba5 100644
--- a/base_logic/lib/na_invariants.v
+++ b/base_logic/lib/na_invariants.v
@@ -5,7 +5,7 @@ Import uPred.
 
 (* Non-atomic ("thread-local") invariants. *)
 
-Definition thread_id := gname.
+Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
   tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
@@ -13,12 +13,12 @@ Class na_invG Σ :=
 Section defs.
   Context `{invG Σ, na_invG Σ}.
 
-  Definition na_own (tid : thread_id) (E : coPset) : iProp Σ :=
-    own tid (CoPset E, ∅).
+  Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
+    own p (CoPset E, ∅).
 
-  Definition na_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
+  Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
     (∃ i, ⌜i ∈ ↑N⌝ ∧
-          inv N (P ∗ own tid (∅, GSet {[i]}) ∨ na_own tid {[i]}))%I.
+          inv N (P ∗ own p (∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
 End defs.
 
 Instance: Params (@na_inv) 3.
@@ -27,36 +27,36 @@ Typeclasses Opaque na_own na_inv.
 Section proofs.
   Context `{invG Σ, na_invG Σ}.
 
-  Global Instance na_own_timeless tid E : TimelessP (na_own tid E).
+  Global Instance na_own_timeless p E : TimelessP (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
 
-  Global Instance na_inv_ne tid N n : Proper (dist n ==> dist n) (na_inv tid N).
+  Global Instance na_inv_ne p N n : Proper (dist n ==> dist n) (na_inv p N).
   Proof. rewrite /na_inv. solve_proper. Qed.
-  Global Instance na_inv_proper tid N : Proper ((≡) ==> (≡)) (na_inv tid N).
+  Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance na_inv_persistent tid N P : PersistentP (na_inv tid N P).
+  Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
-  Lemma na_alloc : (|==> ∃ tid, na_own tid ⊤)%I.
+  Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
   Proof. by apply own_alloc. Qed.
 
-  Lemma na_own_disjoint tid E1 E2 : na_own tid E1 -∗ na_own tid E2 -∗ ⌜E1 ⊥ E2⌝.
+  Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ⊥ E2⌝.
   Proof.
     apply wand_intro_r.
     rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
   Qed.
 
-  Lemma na_own_union tid E1 E2 :
-    E1 ⊥ E2 → na_own tid (E1 ∪ E2) ⊣⊢ na_own tid E1 ∗ na_own tid E2.
+  Lemma na_own_union p E1 E2 :
+    E1 ⊥ E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
   Proof.
     intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
   Qed.
 
-  Lemma na_inv_alloc tid E N P : ▷ P ={E}=∗ na_inv tid N P.
+  Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
   Proof.
     iIntros "HP".
-    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
+    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ ↑N)).
@@ -71,14 +71,14 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_open tid E F N P :
+  Lemma na_inv_open p E F N P :
     ↑N ⊆ E → ↑N ⊆ F →
-    na_inv tid N P -∗ na_own tid F ={E}=∗ ▷ P ∗ na_own tid (F∖↑N) ∗
-                       (▷ P ∗ na_own tid (F∖↑N) ={E}=∗ na_own tid F).
+    na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
+                       (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
   Proof.
     rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
     iDestruct "Htlinv" as (i) "[% Hinv]".
-    rewrite [F as X in na_own tid X](union_difference_L (↑N) F) //.
+    rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
     rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
     iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
diff --git a/docs/derived.tex b/docs/derived.tex
index 7be98440a50215057f190bceed0305ecee22ed5b..55cea67985a0a76b63de6dac57461b2101a8f978 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -1,63 +1,62 @@
 \section{Derived constructions}
 
-\subsection{Non-atomic invariants}
+\subsection{Non-atomic (``thread-local'') invariants}
 
 Sometimes it is necessary to maintain invariants that we need to open non-atomically.
-Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice.
-Access to these \emph{non-atomic invariants} is thus guarded by tokens that take the role that masks play for ``normal'', atomic invariants.
-
-One way to think about them is as ``thread-local invariants''.
-For every thread, we have a set of \emph{tokens}.
-By giving up a token, you can obtain the invariant, and vice versa.
-Such invariants can only be opened by their respective thread, and as a consequence they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions).
-To tie the threads and the tokens together, every thread is assigned a \emph{thread ID}.
-Note that these thread IDs are completely fictional, there is no operational aspect to them.
-In principle, the tokens could move between threads; that's not an issue at all.
+Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the ``normal'', atomic invariants.
+The idea is to use tokens\footnote{Very much like the tokens that are used to encode ``normal'', atomic invariants} that guard access to non-atomic invariants.
+Having the token $\NaTokE\pid\mask$ indicates that we can open all invariants in $\mask$.
+The $\pid$ here is the name of the \emph{invariant pool}.
+This mechanism allows us to have multiple, independent pools of invariants that all have their own namespaces.
+
+One way to think about non-atomic invariants is as ``thread-local invariants'',
+where every pool is a thread.
+Every thread thus has its own, independent set of invariants.
+Every thread threads through all the tokens for its own pool, so that each invariant can only be opened in the thread it belongs to.
+As a consequence, they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions) -- after all, there cannot be any races with other threads.
 
 Concretely, this is the monoid structure we need:
 \begin{align*}
-\textdom{TId} \eqdef{}& \nat \\
-\textmon{TTok} \eqdef{}& \textdom{TId} \fpfn \pset{\textdom{InvName}}\\
-\textmon{TDis} \eqdef{}& \textdom{TId} \fpfn \finpset{\textdom{InvName}}
+\textdom{PId} \eqdef{}& \GName \\
+\textmon{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}
 \end{align*}
-For every thread, there is a set of tokens designating which invariants are \emph{enabled} (closed).
+For every pool, there is a set of tokens designating which invariants are \emph{enabled} (closed).
 This corresponds to the mask of ``normal'' invariants.
 We re-use the structure given by namespaces for non-atomic invariants.
 Furthermore, there is a \emph{finite} set of invariants that is \emph{disabled} (open).
 
-We assume a global instance $\Gttok$ of \textmon{TTok}, and an instance $\Gtdis$ of $\textmon{TDis}$.
-Then we can define some sugar for owning tokens:
+Owning tokens is defined as follows:
 \begin{align*}
-\TTokE\tid\mask \eqdef{}& \ownGhost{\Gttok}{ \mapsingleton\tid\mask : \textmon{TTok} } \\
-\TTok\tid \eqdef{}& \TTokE\tid\top
+\NaTokE\pid\mask \eqdef{}& \ownGhost{\pid}{ (\emptyset, \mask) } \\
+\NaTok\pid \eqdef{}& \NaTokE\pid\top
 \end{align*}
 
 Next, we define non-atomic invariants.
 To simplify this construction,we piggy-back into ``normal'' invariants.
 \begin{align*}
-  \NaInv\tid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\Gtdis{\set{\iname}} \lor \TTokE\tid{\set{\iname}}}
+  \NaInv\pid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\pid{(\set{\iname},\emptyset)} \lor \NaTokE\pid{\set{\iname}}}
 \end{align*}
 
 
 We easily obtain:
 \begin{mathpar}
   \axiom
-  {\TRUE \vs[\bot] \Exists\tid. \TTok\tid}
+  {\TRUE \vs[\bot] \Exists\pid. \NaTok\pid}
 
   \axiom
-  {\TTokE\tid{\mask_1 \uplus \mask_2} \Lra \TTokE\tid{\mask_1} * \TTokE\tid{\mask_2}}
+  {\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}}
   
   \axiom
-  {\later\prop  \vs[\namesp] \always\NaInv\tid\namesp\prop}
+  {\later\prop  \vs[\namesp] \always\NaInv\pid\namesp\prop}
 
   \axiom
-  {\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\namesp}{\later\prop}}
+  {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}}
 \end{mathpar}
 from which we can derive
 \begin{mathpar}
   \infer
   {\namesp \subseteq \mask}
-  {\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\mask}{\later\prop * \TTokE\tid{\mask \setminus \namesp}}}
+  {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\mask}{\later\prop * \NaTokE\pid{\mask \setminus \namesp}}}
 \end{mathpar}
 
 
diff --git a/docs/iris.sty b/docs/iris.sty
index 5781d31e72cd3b31cbeabaed4205690f7fc3741a..8578e2e6ac649222d599263dea0952726b8b93a1 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -339,6 +339,9 @@
 \newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
 \newcommand{\infinite}{\textlog{infinite}}
 
+\newcommand\InvName{\textdom{InvName}}
+\newcommand\GName{\textdom{GName}}
+
 \newcommand{\Prop}{\textlog{Prop}}
 \newcommand{\Pred}{\textlog{Pred}}
 
@@ -427,13 +430,11 @@
 \newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
 
 % Non-atomic invariants
-\newcommand*\Gttok{\gname_\textrm{TTok}}
-\newcommand*\Gtdis{\gname_\textrm{TDis}}
-\newcommand*\tid{t}
-\newcommand\NaInv[3]{\textlog{NAInv}^{#1.#2}(#3)}
+\newcommand*\pid{p}
+\newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}
 
-\newcommand*\TTok[1]{{[}\textrm{T}:#1{]}}
-\newcommand*\TTokE[2]{{[}\textrm{T}:#1.#2{]}}
+\newcommand*\NaTok[1]{{[}\textrm{NaInv}:#1{]}}
+\newcommand*\NaTokE[2]{{[}\textrm{NaInv}:#1.#2{]}}
 
 \endinput
 
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 997215f1b968dea78740b6d981524769997b9ded..152313f72e686a12cc5bc962d916f56c88e51b94 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -27,8 +27,8 @@ To instantiate the program logic, the user picks a family of locally contractive
 
 From this, we construct the bifunctor defining the overall resources as follows:
 \begin{align*}
-  \mathcal G \eqdef{}& \nat \\
-  \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
+  \GName \eqdef{}& \nat \\
+  \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
 \end{align*}
 We will motivate both the use of a product and the finite partial function below.
 $\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
@@ -112,10 +112,10 @@ To this end, we use tokens that manage which invariants are currently enabled.
 
 We assume to have the following four CMRAs available:
 \begin{align*}
-  \mathcal I \eqdef{}& \nat \\
-  \textmon{Inv} \eqdef{}& \authm(\mathcal I \fpfn \agm(\latert \iPreProp)) \\
-  \textmon{En} \eqdef{}& \pset{\mathcal I} \\
-  \textmon{Dis} \eqdef{}& \finpset{\mathcal I} \\
+  \InvName \eqdef{}& \nat \\
+  \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
+  \textmon{En} \eqdef{}& \pset{\InvName} \\
+  \textmon{Dis} \eqdef{}& \finpset{\InvName} \\
   \textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)})
 \end{align*}
 The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
@@ -126,7 +126,7 @@ We assume that at the beginning of the verification, instances named $\gname_{\t
 \paragraph{World Satisfaction.}
 We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
 \begin{align*}
-  W \eqdef{}& \Exists I : \mathcal I \fpfn \Prop.
+  W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
   \begin{array}[t]{@{} l}
     \ownGhost{\gname_{\textmon{Inv}}}{\authfull
       \mapComp {\iname}
@@ -471,8 +471,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
 
 The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
 They, too, are lists of $\nat$, the same type as namespaces.
-In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathcal I$, the type of ``plain'' invariant names.
-Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\mathcal I$ is infinite.
+In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of ``plain'' invariant names.
+Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.
 Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
 
 We will overload the notation for invariant assertions for using namespaces instead of names:
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 9a95ee5c896a723d668ce27a506ab672fcae09cb..367f34eaaa077df0ceb77cb5b2d3e7b52297feac 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -17,15 +17,17 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
 (** Proof rules for the sugar *)
-Lemma wp_lam E x ef e Φ :
-  is_Some (to_val e) → Closed (x :b: []) ef →
-  ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
+Lemma wp_lam E x elam e1 e2 Φ :
+  e1 = Lam x elam →
+  is_Some (to_val e2) →
+  Closed (x :b: []) elam →
+  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
 Lemma wp_let E x e1 e2 Φ :
   is_Some (to_val e1) → Closed (x :b: []) e2 →
   ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. apply wp_lam. Qed.
+Proof. by apply wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 Φ :
   is_Some (to_val e1) → Closed [] e2 →
diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 2c9969e7654bdb805af67fd06a0294cc15668989..fa9b8cd257b635200a8e54644faecd74c775e0c5 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -4,13 +4,13 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 
 Definition assert : val :=
-  locked (λ: "v", if: "v" #() then #() else #0 #0)%V. (* #0 #0 is unsafe *)
+  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
 Proof.
-  iIntros "HΦ". rewrite /assert -lock. wp_let. wp_seq.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index 78ba65bcb82a5362b94fc033f01255df1e8bec99..61f8f72524eb58e09a144bf3e9683b80fea76657 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export notation.
 
-Definition newbarrier : val := locked (λ: <>, ref #false)%V.
-Definition signal : val := locked (λ: "x", "x" <- #true)%V.
+Definition newbarrier : val := λ: <>, ref #false.
+Definition signal : val := λ: "x", "x" <- #true.
 Definition wait : val :=
-  locked (rec: "wait" "x" := if: !"x" then #() else "wait" "x")%V.
+  rec: "wait" "x" := if: !"x" then #() else "wait" "x".
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 8b57fb7a71e43c9d5fffc60a84e5a347ab48fba5..2b65b88c7d2d736a7d60b52d142c86e17e0acbdf 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -95,7 +95,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
   {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
   iIntros (HN Φ) "#? HΦ".
-  rewrite -wp_fupd /newbarrier -lock /=. wp_seq. wp_alloc l as "Hl".
+  rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -119,7 +119,7 @@ Qed.
 Lemma signal_spec l P :
   {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
 Proof.
-  rewrite /signal /send /barrier_ctx -lock /=.
+  rewrite /signal /send /barrier_ctx /=.
   iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 097bd7fb667f65e328c4c264466f9ca0f83c6915..72d16f8300607cf998e00ff036993724af1cec15 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -4,12 +4,11 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
 From iris.heap_lang Require Import proofmode notation.
 
-Definition newcounter : val := locked (λ: <>, ref #0)%V.
-Definition incr : val := locked (
-  rec: "incr" "l" :=
+Definition newcounter : val := λ: <>, ref #0.
+Definition incr : val := rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l")%V.
-Definition read : val := locked (λ: "l", !"l")%V.
+    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
+Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
@@ -36,7 +35,7 @@ Section mono_proof.
     heapN ⊥ N →
     {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -72,7 +71,7 @@ Section mono_proof.
     {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
-    rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[?%mnat_included _]%auth_valid_discrete_2.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
@@ -113,7 +112,7 @@ Section contrib_spec.
     {{{ heap_ctx }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat))))
       as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
@@ -147,7 +146,7 @@ Section contrib_spec.
     {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
   Proof.
     iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
-    rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
@@ -159,7 +158,7 @@ Section contrib_spec.
     {{{ n, RET #n; ccounter γ 1 n }}}.
   Proof.
     iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
-    rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
     apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index ea9a11aed2749ecaf0391c18990bb6a1cddb3bed..3c15c0cd533eb5e4c627b3aa1ffcd1d4c4c6c75e 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -5,11 +5,11 @@ Import uPred.
 Definition parN : namespace := nroot .@ "par".
 
 Definition par : val :=
-  locked (λ: "fs",
+  λ: "fs",
     let: "handle" := spawn (Fst "fs") in
     let: "v2" := Snd "fs" #() in
     let: "v1" := join "handle" in
-    ("v1", "v2"))%V.
+    ("v1", "v2").
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 
 Section proof.
@@ -26,7 +26,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
   ⊢ WP par e {{ Φ }}.
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
-  rewrite /par -lock. wp_value. wp_let. wp_proj.
+  rewrite /par. wp_value. wp_let. wp_proj.
   wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
@@ -44,5 +44,3 @@ Proof.
   iSplitL "H1"; by wp_let.
 Qed.
 End proof.
-
-Global Opaque par.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 46bebd09a94c24c547a842d2265b06fee12863f7..20cbb59b4246f6d43a6b99aa5451d934fbdf74f0 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -5,15 +5,15 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 
 Definition spawn : val :=
-  locked (λ: "f",
+  λ: "f",
     let: "c" := ref NONE in
-    Fork ("c" <- SOME ("f" #())) ;; "c")%V.
+    Fork ("c" <- SOME ("f" #())) ;; "c".
 Definition join : val :=
-  locked (rec: "join" "c" :=
+  rec: "join" "c" :=
     match: !"c" with
       SOME "x" => "x"
     | NONE => "join" "c"
-    end)%V.
+    end.
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -50,7 +50,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   heapN ⊥ N →
   {{{ heap_ctx ∗ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn -lock /=.
+  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index f6d0e66fbc3edc7f8a73ce789e44d5ad3acd2248..e9bcad0c6674cf9e939615a7a49124267b7a14ea 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -5,11 +5,11 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
 
-Definition newlock : val := ssreflect.locked (λ: <>, ref #false)%V.
-Definition try_acquire : val := ssreflect.locked (λ: "l", CAS "l" #false #true)%V.
+Definition newlock : val := λ: <>, ref #false.
+Definition try_acquire : val := λ: "l", CAS "l" #false #true.
 Definition acquire : val :=
-  ssreflect.locked (rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l")%V.
-Definition release : val := ssreflect.locked (λ: "l", "l" <- #false)%V.
+  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
+Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -48,7 +48,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock. unlock.
+    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -83,7 +83,7 @@ Section proof.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
     iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
-    rewrite /release. unlock. wp_let. iInv N as (b) "[Hl _]" "Hclose".
+    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
 End proof.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 8e16f24ece3feb0bf022cd93ab2b97c15032008d..e4c691e6bdf45e225bbb70d9300424ed55aa0253 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -7,24 +7,24 @@ From iris.heap_lang.lib Require Export lock.
 Import uPred.
 
 Definition wait_loop: val :=
-  ssreflect.locked (rec: "wait_loop" "x" "lk" :=
+  rec: "wait_loop" "x" "lk" :=
     let: "o" := !(Fst "lk") in
     if: "x" = "o"
       then #() (* my turn *)
-      else "wait_loop" "x" "lk")%V.
+      else "wait_loop" "x" "lk".
 
 Definition newlock : val :=
-  ssreflect.locked (λ: <>, ((* owner *) ref #0, (* next *) ref #0))%V.
+  λ: <>, ((* owner *) ref #0, (* next *) ref #0).
 
 Definition acquire : val :=
-  ssreflect.locked (rec: "acquire" "lk" :=
+  rec: "acquire" "lk" :=
     let: "n" := !(Snd "lk") in
     if: CAS (Snd "lk") "n" ("n" + #1)
       then wait_loop "n" "lk"
-      else "acquire" "lk")%V.
+      else "acquire" "lk".
 
 Definition release : val :=
-  ssreflect.locked (λ: "lk", (Fst "lk") <- !(Fst "lk") + #1)%V.
+  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
 
 (** The CMRAs we need. *)
 Class tlockG Σ :=
@@ -77,7 +77,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock. unlock.
+    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
     iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
@@ -145,7 +145,7 @@ Section proof.
     iIntros (Φ) "(Hl & Hγ & HR) HΦ".
     iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
     iDestruct "Hγ" as (o) "Hγo".
-    rewrite /release. unlock. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
+    rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index debbf0ed3f26e503726ec7326bdabe01d24c8071..8aef508f3a6e21be8aab5ffc41b36e34181c8fbd 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -111,12 +111,6 @@ Proof.
   intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} :
-  e1 = of_val $ locked (RecV f x erec) →
-  is_Some (to_val e2) →
-  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. unlock. auto using wp_rec. Qed.
-
 Lemma wp_un_op E op e v v' Φ :
   to_val e = Some v →
   un_op_eval op v = Some v' →
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 040c5ae21dd112a6e83b96a04f3fc27e9ffc92a2..bd2bb6ff4cf2c9a3344136759983785d871f46ec 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -47,7 +47,7 @@ Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_sco
 Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
 Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
   (at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
+Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
   (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (at level 200, e1, e2, e3 at level 200) : expr_scope.
@@ -58,20 +58,20 @@ defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
 Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%E))
   (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
+Notation "'rec:' f x y := e" := (locked (RecV f%bind x%bind (Lam y%bind e%E)))
   (at level 102, f, x, y at level 1, e at level 200) : val_scope.
 Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
+Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
   (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
 
 Notation "λ: x , e" := (Lam x%bind e%E)
   (at level 102, x at level 1, e at level 200) : expr_scope.
 Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "λ: x , e" := (LamV x%bind e%E)
+Notation "λ: x , e" := (locked (LamV x%bind e%E))
   (at level 102, x at level 1, e at level 200) : val_scope.
-Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
+Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
   (at level 102, x, y, z at level 1, e at level 200) : val_scope.
 
 Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index bc647d8e44c8726d4107761f3905b3db0713d988..65fff20b5bbeec940954bcb3045ac84071b5f477 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -44,13 +44,21 @@ Tactic Notation "wp_value" :=
   | _ => fail "wp_value: not a wp"
   end.
 
+Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
+Proof. by unlock. Qed.
+
+(* Applied to goals that are equalities of expressions. Will try to unlock the
+   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
+Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
+
 Tactic Notation "wp_rec" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind_core K; etrans; [|(eapply wp_rec; wp_done) || (eapply wp_rec_locked; wp_done)]; simpl_subst; wp_finish
+    wp_bind_core K; etrans;
+      [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
 (*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
   | _ => fail "wp_rec: not a 'wp'"
   end.
@@ -60,7 +68,8 @@ Tactic Notation "wp_lam" :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind_core K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
+    wp_bind_core K; etrans;
+      [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
 (*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
   | _ => fail "wp_lam: not a 'wp'"
   end.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 7ca9b524a148ede613bda213d22c21c3d99afe1f..20006310255fae0abd6942310730d3d87fa34d52 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -66,7 +66,7 @@ Ltac done :=
     | discriminate
     | contradiction
     | split
-    | match goal with H : ¬_ |- _ => case H; clear H; done end
+    | match goal with H : ¬_ |- _ => case H; clear H; fast_done end
     ]
   ].
 Tactic Notation "by" tactic(tac) :=
@@ -214,8 +214,8 @@ Tactic Notation "csimpl" "in" "*" :=
 and injects equalities, and tries to contradict impossible inequalities. *)
 Tactic Notation "simplify_eq" := repeat
   match goal with
-  | H : _ ≠ _ |- _ => by destruct H
-  | H : _ = _ → False |- _ => by destruct H
+  | H : _ ≠ _ |- _ => by case H; clear H
+  | H : _ = _ → False |- _ => by case H; clear H
   | H : ?x = _ |- _ => subst x
   | H : _ = ?x |- _ => subst x
   | H : _ = _ |- _ => discriminate H
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 1800ad32cce040545e4fcbc44022634cf6552087..d9f173c180f0dabcb15ac7e8dc3bc0b0cc091cbd 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -54,8 +54,6 @@ Section client.
 Qed.
 End client.
 
-Global Opaque worker client.
-
 Section ClosedProofs.
 
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
diff --git a/tests/counter.v b/tests/counter.v
index 4b852ad6d87237bfba33030ed24f7260f47c0032..a97e466e26e575398b00388fe2e1231692878290 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -136,5 +136,3 @@ Proof.
   iModIntro; rewrite /C; eauto 10 with omega.
 Qed.
 End proof.
-
-Global Opaque newcounter incr read.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 1ba0ee98bf1d45f839cf552dfd0f766980fec9c8..60160c224cbf04d9404d613d54ea3e13b5d7efbc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -37,7 +37,6 @@ Section LiftingTests.
   Definition Pred : val :=
     λ: "x",
       if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
-  Global Opaque FindPred Pred.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 →
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 7000179672758fafb898385ab0bb3f54c10f74e1..2a143a107b42abb8241c6e9ef4ba234a04057767 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -97,5 +97,3 @@ Proof.
   - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
 Qed.
 End proof.
-
-Global Opaque client.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 64565e93fa8e9047cf8fe087829c52ed5851227c..10cc5bf35b46470162ce0ac0734aa1f89c46f7e0 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -24,7 +24,6 @@ Definition rev : val :=
        "l" <- ("tmp1", "acc");;
        "rev" "tmp2" "hd"
     end.
-Global Opaque rev.
 
 Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) :
   heap_ctx ∗ is_list hd xs ∗ is_list acc ys ∗
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 323f8896aec983c45a528aa2f90f8ff70e0f28f2..0f7b99c73d6626db07d8240972e63209f0676d69 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -96,5 +96,3 @@ Proof.
     iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
 Qed.
 End proof.
-
-Global Opaque one_shot_example.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index bc216d6538ab7a62120fb5aaf23b54e6077c7ff0..0f38392204e601f68c806ec3e93f897827f03030 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -64,6 +64,3 @@ Proof.
   rewrite Z.add_0_r.
   iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
 Qed.
-
-Global Opaque sum_loop sum'.
-