Extension of the recursive notations mechanism

- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 41 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 2e136edf1..57d8ebbc4 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -24,3 +24,44 @@ Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
 Remove Printing Let prod.
 Check match (0,0,0) with (x,y,z) => x+y+z end.
 Check let '(a,b,c) := ((2,3),4) in a.
+
+(* Test notations with binders *)
+
+Notation "∃  x .. y , P":=
+  (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+
+Check (∃ n p, n+p=0).
+
+Notation "∀  x .. y , P":= (forall x, .. (forall y, P) ..)
+  (x binder, at level 200, right associativity).
+
+Check (∀ n p, n+p=0).
+
+Notation "'λ'  x .. y , P":= (fun x, .. (fun y, P) ..)
+  (y binder, at level 200, right associativity).
+
+Check (λ n p, n+p=0).
+
+Generalizable Variable A.
+
+Check `(λ n p : A, n=p).
+Check `(∃ n p : A, n=p).
+Check `(∀ n p : A, n=p).
+
+Notation "'let'' f x .. y  :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (f ident, x closed binder, y closed binder, at level 200,
+   right associativity).
+
+Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
+
+(* This one is not fully satisfactory because binders in the same type
+   are re-factorized and parentheses are needed even for atomic binder
+
+Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (f ident, x closed binder, y closed binder, at level 200,
+   right associativity).
+
+Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
+*)