diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index d8e4a6618c5d54172c91b48ebbbf5d69a65e7b21..b3b5902ff78e354ed8fb17153283c40c6b3071fa 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -4,3 +4,4 @@ Definition newbarrier : val := λ: <>, ref #0.
 Definition signal : val := λ: "x", '"x" <- #1.
 Definition wait : val :=
   rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
+Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index b0707a29cbb4ac752352a8fba695ed3875c4169a..df476fbf411578ea71696da13e268aa756cb5c44 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -8,6 +8,7 @@ Definition acquire : val :=
   rec: "acquire" "l" :=
     if: CAS '"l" #false #true then #() else '"acquire" '"l".
 Definition release : val := λ: "l", '"l" <- #false.
+Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 8f1812620c6424f8b5ab8fca66baaad35ce17185..e394bfc471b923bde4958c6c39aa9f8c97021fb6 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -14,7 +14,7 @@ Infix "||" := Par : expr_scope.
 Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
 Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
   WSubst x es H par par := do_wsubst_closed _ x es H _.
-Typeclasses Opaque par.
+Global Opaque par.
 
 Section proof.
 Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 294325be7dd0e756bed3b05f7b5fea73fcff3723..b2f5f24beb19b4def7281d5370c93c726446a98c 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -13,6 +13,7 @@ Definition join : val :=
       InjR "x" => '"x"
     | InjL <>  => '"join" '"c"
     end.
+Global Opaque spawn join.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 50b67fcc52c9c5440411f6d2de33b48ee2d50418..62d1b3d6d0b89df583506305eaece9ee1389bf0b 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -196,4 +196,3 @@ Ltac simpl_subst :=
 Arguments wexpr : simpl never.
 Arguments subst : simpl never.
 Arguments wsubst : simpl never.
-Arguments of_val : simpl never.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 06e7761565a0d616152d304d30c7c4863022b352..2411087c3d92d5eaa58f74bca73b7eef1aaa91bf 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,7 +9,7 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
+Ltac wp_done := rewrite /= ?to_of_val; fast_done.
 
 Ltac wp_value_head :=
   match goal with
@@ -23,7 +23,7 @@ Ltac wp_value_head :=
   end.
 
 Ltac wp_finish := intros_revert ltac:(
-  rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
+  rewrite /= ?to_of_val; try strip_later; try wp_value_head).
 
 Tactic Notation "wp_value" :=
   lazymatch goal with
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 0338d3e075272b7f5c226bd3fd4559012b575918..ca07236f2934682a3f01dc886718d89070dad283 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -11,6 +11,7 @@ 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 {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 22cabb3ecb52361cfb12114ab8e48fa1a4700c90..f83c8a8d739a4ec2b2222f1053a774fe4b6cdcbc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -37,6 +37,7 @@ 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 377ebcf524a13f851ba7bf0ac3e4846037608149..969586fdfc58924cc7da9010ed137109ca7654bf 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -7,6 +7,7 @@ Import uPred.
 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 (G : cFunctor).
diff --git a/tests/one_shot.v b/tests/one_shot.v
index a96ffa375e373a0e6049e02202a641e45ea24c92..89dd05d948ffbf573e55ebb8b388f27f5451fc9c 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -18,6 +18,7 @@ Definition one_shot_example : val := λ: <>,
        | InjR "m" => Assert ('"n" = '"m")
        end
     end)).
+Global Opaque one_shot_example.
 
 Class one_shotG Σ :=
   OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.