diff --git a/barrier/client.v b/barrier/client.v
index 51c2ba046cd9817e75291ad018fa9f7b7fffeab3..8493373c9690183207b261ae0629f7652bbb2e46 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -2,10 +2,13 @@ From barrier Require Import proof.
 From program_logic Require Import auth sts saved_prop hoare ownership.
 Import uPred.
 
-Definition worker (n : Z) := (λ: "b" "y", wait "b" ;; (!"y") 'n)%L.
-Definition client := (let: "y" := ref '0 in let: "b" := newbarrier '() in
-                      Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;;
-                      "y" <- (λ: "z", "z" + '42) ;; signal "b")%L.
+Definition worker (n : Z) : val :=
+  λ: "b" "y", wait "b" ;; !"y" 'n.
+Definition client : expr :=
+  let: "y" := ref '0 in
+  let: "b" := newbarrier '() in
+  Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;;
+  "y" <- (λ: "z", "z" + '42) ;; signal "b".
 
 Section client.
   Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index f79f159762bed09cb0e798024e5d656e0ab59772..d0b24bc0e18930b06bb7d7961b035786d1dbab2f 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -24,14 +24,14 @@ Coercion of_val : val >-> expr.
    are not put in any scope so as to avoid lots of annoying %L scopes while
    pretty printing. *)
 Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
-Notation "' l" := (Lit l%Z) (at level 8, format "' l").
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
   (Case e0 x1 e1 x2 e2)
   (e0, x1, e1, x2, e2 at level 200) : lang_scope.
+Notation "' l" := (Lit l%Z) (at level 8, format "' l").
 Notation "' l" := (LitV l%Z) (at level 8, format "' l").
 Notation "'()"  := (Lit LitUnit) (at level 0).
 Notation "'()"  := (LitV LitUnit) (at level 0).
-Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
+Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope.
 Notation "'ref' e" := (Alloc e%L)
   (at level 30, right associativity) : lang_scope.
 Notation "- e" := (UnOp MinusUnOp e%L)