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 b5ee9c9c39920d2bf053a25bb5c1e150aa0791cf..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.
@@ -293,12 +291,12 @@ Qed.
 Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
 Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
 
-Lemma values_head_stuck e1 σ1 e2 σ2 ef :
+Lemma val_head_stuck e1 σ1 e2 σ2 ef :
   head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
-Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
+Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
 
 Lemma atomic_not_val e : atomic e → to_val e = None.
 Proof. destruct e; naive_solver. Qed.
@@ -326,7 +324,7 @@ Lemma atomic_step e1 σ1 e2 σ2 ef :
   atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
 Proof.
   intros Hatomic [K e1' e2' -> -> Hstep].
-  assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
+  assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
   naive_solver eauto using atomic_head_step.
 Qed.
 
@@ -357,7 +355,7 @@ Proof.
   { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
       eauto using fill_not_val, head_ctx_step_val. }
   cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
-  eauto using fill_item_no_val_inj, values_head_stuck, fill_not_val.
+  eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val.
 Qed.
 
 Lemma alloc_fresh e v σ :
@@ -373,7 +371,7 @@ Program Canonical Structure heap_lang : language := {|
   atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
+  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
 
 Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
 Proof.
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/tactics.v b/heap_lang/tactics.v
index 278d76aec06d4270d35757fb7d47aa65a541e3e4..359c4c2b2051296b4dbd7c96fa6d128635679363 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -19,7 +19,7 @@ Ltac inv_step :=
      simpl in H; first [subst e|discriminate H|injection H as H]
      (* ensure that we make progress for each subgoal *)
   | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
-    apply values_head_stuck, (fill_not_val K) in H;
+    apply val_head_stuck, (fill_not_val K) in H;
     by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
   | H : head_step ?e _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if e is a variable
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).
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 0a0156feb73b3ee919fa317d5af34e0a1cf275af..14c93e4d8d9a1f5809accff70b02a8429ef8733b 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -33,7 +33,7 @@ Proof.
     (Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
   rewrite wp_eq in Hwp.
   destruct (wp_step_inv ⊤ ∅ Φ e1 (k + n) (S (k + n)) σ1 r
-    (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
+    (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using val_stuck.
   { by rewrite right_id_L -big_op_cons Permutation_middle. }
   destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
   revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
diff --git a/program_logic/language.v b/program_logic/language.v
index 4bd4301310537c876f9f642814f456f38a639d5c..57a4859ba9ec01fe84cfc412131119785f7c4822 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -10,7 +10,7 @@ Structure language := Language {
   prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
+  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
   atomic_not_val e : atomic e → to_val e = None;
   atomic_step e1 σ1 e2 σ2 ef :
     atomic e1 →
@@ -23,7 +23,7 @@ Arguments atomic {_} _.
 Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
-Arguments values_stuck {_} _ _ _ _ _ _.
+Arguments val_stuck {_} _ _ _ _ _ _.
 Arguments atomic_not_val {_} _ _.
 Arguments atomic_step {_} _ _ _ _ _ _ _.
 
@@ -45,7 +45,7 @@ Section language.
        step ρ1 ρ2.
 
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
-  Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
+  Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
   Lemma atomic_of_val v : ¬atomic (of_val v).
   Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Inj (=) (=) (@of_val Λ).