diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index bbe0624c8c01790f2236e32b6ad93f7b007c6687..1789ac8f31a0cd8063aa3b40f0168979567c3298 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -35,7 +35,6 @@ Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
 
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
 Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
-Notation "^^ e" := (wexpr' e%E) (at level 8, format "^^ e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)