diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index cd621a876f44085f36d2c1df4a5efe1c8daf0c2c..0b4905002c9450b94bcdc45a01dfaf04fb01ac8a 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -86,6 +86,14 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  ============================
+  --------------------------------------∗
+  WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 69c99fab2baa525bc758bc63a3d150951dd87b50..041b177baa2ca907e531981444618d26fc84b3ca 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -149,6 +149,12 @@ End tests.
 Section printing_tests.
   Context `{!heapG Σ}.
 
+  Lemma ref_print :
+    True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
   (* These terms aren't even closed, but that's not what this is about.  The
   length of the variable names etc. has been carefully chosen to trigger
   particular behavior of the Coq pretty printer. *)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index c5b85612b7397785017425253cb4fad3b97db3a5..81e3fc3e54f5ffb8d3f8b83bd8177d67148096d5 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -59,8 +59,7 @@ Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
 
 Notation "()" := LitUnit : val_scope.
 Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
-Notation "'ref' e" := (Alloc e%E)
-  (at level 30, right associativity) : expr_scope.
+Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
 Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.
 
 Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.