diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index f7ff70f72df31b99e71fe6340c3a63403882ab14..72aa0f2ebcd4185dc62d1d9b9060ca86baff3484 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -15,6 +15,7 @@ Coercion of_val : val >-> expr.
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
 (* What about Arguments for hoare triples?. *)
+Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope.
 Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
 Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
 Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.