diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index 5ed15fdc6c1c524634a4e2e368dc84046c9af2fe..fbb0b4a1af0c34c141b7cda84ce6bda48d2976f5 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -47,7 +47,7 @@ Module notations.
   Notation "λ: x , e" := (Lam x e%L)
     (at level 102, x at level 1, e at level 200) : lang_scope.
   Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
-    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
+    (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
   Notation "e1 ; e2" := (Lam "" e2%L e1%L)
     (at level 100, e2 at level 200) : lang_scope.
 End notations.