Made notations for exists, exists! and notations of Utf8.v recursive notations

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

1 files changed, 8 insertions, 12 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 14832e0b72..97f3b126cc 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -216,11 +216,9 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
 
 (* Rule order is important to give printing priority to fully typed exists *)
 
-Notation "'exists' x , p" := (ex (fun x => p))
-  (at level 200, x ident, right associativity) : type_scope.
-Notation "'exists' x : t , p" := (ex (fun x:t => p))
-  (at level 200, x ident, right associativity,
-    format "'[' 'exists'  '/  ' x  :  t ,  '/  ' p ']'")
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  (at level 200, x binder, right associativity,
+   format "'[' 'exists'  '/  ' x .. y ,  '/  ' p ']'")
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
@@ -390,13 +388,11 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
 
 (** Unique existence *)
 
-Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
-  (at level 200, x ident, right associativity,
-    format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" :=
-  (ex (unique (fun x:A => P)))
-  (at level 200, x ident, right associativity,
-    format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
+Notation "'exists' ! x .. y , p" :=
+  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
+  (at level 200, x binder, right associativity,
+   format "'[' 'exists'  !  '/  ' x .. y ,  '/  ' p ']'")
+  : type_scope.
 
 Lemma unique_existence : forall (A:Type) (P:A->Prop),
   ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).