diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index f850174c4be0de12592406ac6f3b08ad55c2e0a0..8f6bac10b0424eb691f7303a195af81432b429a2 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -59,24 +59,6 @@ Inductive expr :=
   | CAS (e0 : expr) (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
-Delimit Scope expr_scope with E.
-Arguments Rec _ _ _%E.
-Arguments App _%E _%E.
-Arguments Lit _.
-Arguments UnOp _ _%E.
-Arguments BinOp _ _%E _%E.
-Arguments If _%E _%E _%E.
-Arguments Pair _%E _%E.
-Arguments Fst _%E.
-Arguments Snd _%E.
-Arguments InjL _%E.
-Arguments InjR _%E.
-Arguments Case _%E _%E _%E.
-Arguments Fork _%E.
-Arguments Alloc _%E.
-Arguments Load _%E.
-Arguments Store _%E _%E.
-Arguments CAS _%E _%E _%E.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
@@ -105,10 +87,6 @@ Inductive val :=
   | InjRV (v : val).
 
 Bind Scope val_scope with val.
-Delimit Scope val_scope with V.
-Arguments PairV _%V _%V.
-Arguments InjLV _%V.
-Arguments InjRV _%V.
 
 Fixpoint of_val (v : val) : expr :=
   match v with
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 50e2c21f0e0ac3f0016c36c85a52aebe3338bdd1..81195b9d45925781a5ab1d263067d1296b1c09cb 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -53,6 +53,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
+  (* TODO: Coq is printing %V here.  *)
   wp_let. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 45e6932a429dd813e5fda1eb0e564c03f79e73fe..600cca0a3679c6dfd00b3b5579c168ffe2669c08 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,22 +1,6 @@
 From iris.heap_lang Require Export derived.
 Export heap_lang.
 
-Arguments wp {_ _ _} _ _%E _.
-
-Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'WP'  e  {{  Φ  } }") : uPred_scope.
-
-Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
-
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/program_logic/language.v b/program_logic/language.v
index 04bba2a4a4dc635d74a676aebd8b8f650c327afe..cd33108da2ea94c753a0081d1361f5565391fca9 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -11,6 +11,10 @@ Structure language := Language {
   of_to_val e v : to_val e = Some v → of_val v = e;
   val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
 }.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+Bind Scope expr_scope with expr.
+Bind Scope expr_scope with val.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
 Arguments prim_step {_} _ _ _ _ _.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 3026e7e71e16e0f04f8f1d957b565270c67c9d90..2e94c9ccd23e192a8bdc22aac665e5bd83f2e409 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -33,20 +33,20 @@ Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
 Definition wp := proj1_sig wp_aux.
 Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
 
-Arguments wp {_ _ _} _ _ _.
+Arguments wp {_ _ _} _ _%E _.
 Instance: Params (@wp) 5.
 
-Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
+Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
-Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
+Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
+Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.