diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 547f961589011b808f2ad2867c196fda6c693380..4de01916978890d3f724198d976f7f24b96eedbe 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -7,7 +7,6 @@ Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
-Global Opaque assert.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
@@ -15,3 +14,5 @@ Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
+
+Global Opaque assert.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 2b65b88c7d2d736a7d60b52d142c86e17e0acbdf..b67477be273dba7d8ad4f7ef60b92e61bc77f4ce 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -22,6 +22,8 @@ Section proof.
 Context `{!heapG Σ, !barrierG Σ} (N : namespace).
 Implicit Types I : gset gname.
 
+Local Transparent newbarrier signal wait.
+
 Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
   (∃ Ψ : gname → iProp Σ,
     ▷ (P -∗ [∗ set] i ∈ I, Ψ i) ∗ [∗ set] i ∈ I, saved_prop_own i (Ψ i))%I.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 941ae644e63957e44b543b27efa22a42422477cf..4391887a83a1d986acb48cf749a94ced4afca64a 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -10,7 +10,6 @@ Definition incr : val :=
     let: "n" := !"l" in
     if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
-Global Opaque newcounter incr get.
 
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
@@ -167,3 +166,5 @@ Section contrib_spec.
     by iApply "HΦ".
   Qed.
 End contrib_spec.
+
+Global Opaque newcounter incr get.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 52eae597b108dfdbbde653fc3edfb4966fdf4c12..6b4b310aa4419c7b7115bf5ee6caa478e0295cac 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -11,7 +11,6 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
-Global Opaque par.
 
 Section proof.
 Context `{!heapG Σ, !spawnG Σ}.
@@ -45,3 +44,5 @@ 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 17c44630afcac7feefd5c13ff4b03a07efd62a03..d424aa7fa97158264d3319cb871eb23500519d29 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -14,7 +14,6 @@ Definition join : val :=
       SOME "x" => "x"
     | NONE => "join" "c"
     end.
-Global Opaque spawn join.
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -79,3 +78,4 @@ Qed.
 End proof.
 
 Typeclasses Opaque join_handle.
+Global Opaque spawn join.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 896caade9b443561c74bb15dde8cd87c44ba57dd..46e8715bc8da31651a88d9c152e2f117740e3cc4 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -10,7 +10,6 @@ Definition try_acquire : val := λ: "l", CAS "l" #false #true.
 Definition acquire : val :=
   rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
 Definition release : val := λ: "l", "l" <- #false.
-Global Opaque newlock try_acquire acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -89,6 +88,9 @@ Section proof.
   Qed.
 End proof.
 
+Typeclasses Opaque is_lock locked.
+Global Opaque newlock try_acquire acquire release.
+
 Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 194b3da1f38fd94331f7b3b3a84c5b6d45409b98..eab626e5605e53312d8f0b0fbf676879f9809255 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -25,8 +25,6 @@ Definition acquire : val :=
 Definition release : val := λ: "lk",
   (Fst "lk") <- !(Fst "lk") + #1.
 
-Global Opaque newlock acquire release wait_loop.
-
 (** The CMRAs we need. *)
 Class tlockG Σ :=
   tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
@@ -170,6 +168,7 @@ Section proof.
 End proof.
 
 Typeclasses Opaque is_lock issued locked.
+Global Opaque newlock acquire release wait_loop.
 
 Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 6b60585dc9f43e65c0640038cd9185781543c2ed..1800ad32cce040545e4fcbc44022634cf6552087 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -11,7 +11,6 @@ Definition client : expr :=
   let: "b" := newbarrier #() in
   ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
     (worker 12 "b" "y" ||| worker 17 "b" "y").
-Global Opaque worker client.
 
 Section client.
   Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
@@ -55,6 +54,8 @@ 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 9bc8d14b9a54f82eaffde6ea6c98516ef64dbbd8..4b852ad6d87237bfba33030ed24f7260f47c0032 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -16,7 +16,6 @@ Definition incr : val :=
     let: "n" := !"l" in
     if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
-Global Opaque newcounter incr read.
 
 (** The CMRA we need. *)
 Inductive M := Auth : nat → M | Frag : nat → M | Bot.
@@ -137,3 +136,5 @@ Proof.
   iModIntro; rewrite /C; eauto 10 with omega.
 Qed.
 End proof.
+
+Global Opaque newcounter incr read.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 0c3f3cb3f6d473b436e751e23c803cc2c6f9f378..7000179672758fafb898385ab0bb3f54c10f74e1 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -21,7 +21,6 @@ Proof. apply subG_inG. Qed.
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
   (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
-Global Opaque client.
 
 Section proof.
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
@@ -98,3 +97,5 @@ Proof.
   - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
 Qed.
 End proof.
+
+Global Opaque client.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 04c0354c25c0dd4cbb80bd02e53500108dabba7e..323f8896aec983c45a528aa2f90f8ff70e0f28f2 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -18,7 +18,6 @@ Definition one_shot_example : val := λ: <>,
        | SOME "m" => assert: "n" = "m"
        end
     end)).
-Global Opaque one_shot_example.
 
 Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
 Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
@@ -97,3 +96,5 @@ 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 8e3b9b9c4fabc88f574429062169fb5135f65376..bc216d6538ab7a62120fb5aaf23b54e6077c7ff0 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -33,8 +33,6 @@ Definition sum' : val := λ: "t",
   sum_loop "t" "l";;
   !"l".
 
-Global Opaque sum_loop sum'.
-
 Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) :
   heap_ctx ∗ l ↦ #n ∗ is_tree v t
     ∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #())
@@ -66,3 +64,6 @@ Proof.
   rewrite Z.add_0_r.
   iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
 Qed.
+
+Global Opaque sum_loop sum'.
+