diff --git a/barrier/proof.v b/barrier/proof.v
index b849ce969d2350a54ba6b134f7da9bdc357bedba..c06561771944d95997f55b2ed1b0d2bcc17a4f0e 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -206,7 +206,7 @@ Proof.
   apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
   rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
   apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?.
-  wp_focus (! _)%L.
+  wp_focus (! _)%E.
   (* I think some evars here are better than repeating *everything* *)
   eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
     eauto with I ndisj.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index ac052cc6150f778f9c5f6b462e9135a0e8b111d5..77abc0de183c22e7309e1425f839fe92e356d7c2 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -19,10 +19,6 @@ Inductive binder := BAnon | BNamed : string → binder.
 
 Delimit Scope binder_scope with binder.
 Bind Scope binder_scope with binder.
-Delimit Scope lang_scope with L.
-Bind Scope lang_scope with base_lit.
-Delimit Scope val_scope with V.
-Bind Scope val_scope with base_lit.
 
 Inductive expr :=
   (* Base lambda calculus *)
@@ -51,6 +47,9 @@ Inductive expr :=
   | Store (e1 : expr) (e2 : expr)
   | Cas (e0 : expr) (e1 : expr) (e2 : expr).
 
+Bind Scope expr_scope with expr.
+Delimit Scope expr_scope with E.
+
 Inductive val :=
   | RecV (f x : binder) (e : expr) (* e should be closed *)
   | LitV (l : base_lit)
@@ -59,9 +58,8 @@ Inductive val :=
   | InjRV (v : val)
   | LocV (l : loc).
 
-Bind Scope binder_scope with expr.
-Bind Scope lang_scope with expr base_lit.
-Bind Scope val_scope with val base_lit.
+Bind Scope val_scope with val.
+Delimit Scope val_scope with V.
 
 Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
 Proof. solve_decision. Defined.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 1ea9ae21e822e72ee215cfc8f59ebcc45a0bfc1d..ad55bee90c2785ccc17b93123745eab71cd4e439 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,10 +1,10 @@
 From heap_lang Require Export derived.
 
-Arguments wp {_ _} _ _%L _.
-Notation "|| e @ E {{ Φ } }" := (wp E e%L Φ)
+Arguments wp {_ _} _ _%E _.
+Notation "|| e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "||  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "|| e {{ Φ } }" := (wp ⊤ e%L Φ)
+Notation "|| e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "||  e   {{  Φ  } }") : uPred_scope.
 
@@ -19,72 +19,71 @@ Coercion of_val : val >-> expr.
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
 
-(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
-    first. *)
-
 (* No scope, does not conflict and scope is often not inferred properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "% l" := (LocV l) (at level 8, format "% l").
 
-Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
   (Match e0 x1 e1 x2 e2)
-  (e0, x1, e1, x2, e2 at level 200) : lang_scope.
+  (e0, x1, e1, x2, e2 at level 200) : expr_scope.
 Notation "()" := LitUnit : val_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)
-  (at level 35, right associativity) : lang_scope.
-Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
-  (at level 50, left associativity) : lang_scope.
-Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
-  (at level 50, left associativity) : lang_scope.
-Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
-Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
-Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
-Notation "~ e" := (UnOp NegOp e%L) (at level 75, right associativity) : lang_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 "- e" := (UnOp MinusUnOp e%E)
+  (at level 35, right associativity) : expr_scope.
+Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
+  (at level 50, left associativity) : expr_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
+  (at level 50, left associativity) : expr_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
+Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
-Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
-Notation "'rec:' f x := e" := (Rec f x e%L)
-  (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
-Notation "'rec:' f x := e" := (RecV f x e%L)
+Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
+Notation "'rec:' f x := e" := (Rec f x e%E)
+  (at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f x := e" := (RecV f x e%E)
   (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
-Notation "'if:' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
-  (at level 200, e1, e2, e3 at level 200) : lang_scope.
+Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
+  (at level 200, e1, e2, e3 at level 200) : expr_scope.
 
 (** Derived notions, in order of declaration. The notations for let and seq
 are stated explicitly instead of relying on the Notations Let and Seq as
 defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
-Notation "λ: x , e" := (Lam x e%L)
-  (at level 102, x at level 1, e at level 200) : lang_scope.
-Notation "λ: x , e" := (LamV x e%L)
+Notation "λ: x , e" := (Lam x e%E)
+  (at level 102, x at level 1, e at level 200) : expr_scope.
+Notation "λ: x , e" := (LamV x e%E)
   (at level 102, x at level 1, e at level 200) : val_scope.
 
-Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
-  (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
-Notation "e1 ;; e2" := (Lam BAnon e2%L e1%L)
-  (at level 100, e2 at level 200, format "e1  ;;  e2") : lang_scope.
+Notation "'let:' x := e1 'in' e2" := (Lam x e2%E e1%E)
+  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
 (* These are not actually values, but we want them to be pretty-printed. *)
-Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
+Notation "'let:' x := e1 'in' e2" := (LamV x e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
-Notation "e1 ;; e2" := (LamV BAnon e2%L e1%L)
+Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
 
-Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
-  (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
-Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L))
+Notation "'rec:' f x y := e" := (Rec f x (Lam y e%E))
+  (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f x y := e" := (RecV f x (Lam y e%E))
   (at level 102, f, x, y at level 1, e at level 200) : val_scope.
-Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
-  (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
-Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
+Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%E)))
+  (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%E)))
   (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
-Notation "λ: x y , e" := (Lam x (Lam y e%L))
-  (at level 102, x, y at level 1, e at level 200) : lang_scope.
-Notation "λ: x y , e" := (LamV x (Lam y e%L))
+Notation "λ: x y , e" := (Lam x (Lam y e%E))
+  (at level 102, x, y at level 1, e at level 200) : expr_scope.
+Notation "λ: x y , e" := (LamV x (Lam y e%E))
   (at level 102, x, y at level 1, e at level 200) : val_scope.
-Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%L)))
-  (at level 102, x, y, z at level 1, e at level 200) : lang_scope.
-Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%L)))
+Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%E)))
+  (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
+Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%E)))
   (at level 102, x, y, z at level 1, e at level 200) : val_scope.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 54baf3fe7d003701af24916862a52a39ceef352f..45901ad1adb3d9ad183f46dc21e42e2f4cfa42ea 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -4,7 +4,7 @@ From heap_lang Require Import wp_tactics heap notation.
 Import uPred.
 
 Section LangTests.
-  Definition add := (#21 + #21)%L.
+  Definition add := (#21 + #21)%E.
   Goal ∀ σ, prim_step add σ (#42) σ None.
   Proof. intros; do_step done. Qed.
   Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0).
@@ -14,7 +14,7 @@ Section LangTests.
     by eapply (Ectx_step  _ _ _ _ _ []), (BetaS _ _ _ _ #0).
   Qed.
   Definition lam : expr := λ: "x", "x" + #21.
-  Goal ∀ σ, prim_step (lam #21)%L σ add σ None.
+  Goal ∀ σ, prim_step (lam #21)%E σ add σ None.
   Proof.
     intros. rewrite /lam. (* FIXME: do_step does not work here *)
     by eapply (Ectx_step  _ _ _ _ _ []), (BetaS <> "x" ("x" + #21) _ #21).