From 04f588de0951f39385380bd8bb9c85b24755c337 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 26 Feb 2016 23:39:38 +0100 Subject: [PATCH] Add space to pretty printed notation ;; for seq. --- heap_lang/notation.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heap_lang/notation.v b/heap_lang/notation.v index 0361e8022..68cbb353f 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -62,9 +62,9 @@ Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L) Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L) (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. + (at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope. Notation "e1 ;; e2" := (LamV "" e2%L e1%L) - (at level 100, e2 at level 200) : lang_scope. + (at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope. Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L)) (at level 102, f, x, y at level 1, e at level 200) : lang_scope. -- GitLab