From e475fff15d20c5573b560d7290d600260679115c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 10 Feb 2016 23:15:46 +0100 Subject: [PATCH] Fix level for let notation. --- heap_lang/sugar.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v index 5ed15fdc6..fbb0b4a1a 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. -- GitLab