diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eba3026da02e9c6d1bb25b1280f9d8ecbeae799c..54d46b46ef9bc01636f03c15603096acb829056e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -19,6 +19,8 @@ Section tests.
     end.
   Qed.
 
+  Definition val_scope_test_1 := SOMEV (#(), #()).
+
   Definition heap_e : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4a98fbbe8a32a48a7dbff9409aae3e49e81a66c5..41ebd16fb54a01a73a16f2b0dc3c6118916dfbc3 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -66,11 +66,11 @@ Inductive expr :=
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
   | FAA (e1 : expr) (e2 : expr).
 
+Bind Scope expr_scope with expr.
+
 Notation NONE := (InjL (Lit LitUnit)) (only parsing).
 Notation SOME x := (InjR x) (only parsing).
 
-Bind Scope expr_scope with expr.
-
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
   | Var x => bool_decide (x ∈ X)
@@ -97,11 +97,11 @@ Inductive val :=
   | InjLV (v : val)
   | InjRV (v : val).
 
+Bind Scope val_scope with val.
+
 Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
 Notation SOMEV x := (InjRV x) (only parsing).
 
-Bind Scope val_scope with val.
-
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e