From 58ae11eddebe7db90df1788f2a03371d855eb511 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 7 Apr 2019 21:47:42 +0200
Subject: [PATCH] Change the level of `ref` so it's the same as application.

---
 tests/heap_lang.ref           | 8 ++++++++
 tests/heap_lang.v             | 6 ++++++
 theories/heap_lang/notation.v | 3 +--
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index cd621a876..0b4905002 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 69c99fab2..041b177ba 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 c5b85612b..81e3fc3e5 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.
-- 
GitLab