From 15abe33f55b317410223bd48576fa35c81943ff9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 14 Feb 2018 19:55:21 +0100 Subject: Refining the strategy for glueing let-ins to a sequence of binders. To deal with existing notations starting with a "let" (see notation "for" in output/Notation2.v) we adopt the pragmatic approach of glueing only inner let by default. Ideally, it might be nicer to detect if there is an overlap of notation, and not to glue only in case of overlap. We could also decide that a notation starting with a "let" should always be protected by some constant, say "id", so as to avoid possible collisions, but this would require changes user side. --- test-suite/output/Notations2.out | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'test-suite/output') diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 0e5f39903..6ffe56e11 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,8 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), -x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop -- cgit v1.2.3