From 2e67f33bcac10d883879a0cc0a4b7b75b60e473c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Feb 2006 11:28:24 +0000
Subject: Ajout 'exists! x:A, P (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8086 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic.v | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index f50e796827..8a11a43bad 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -141,16 +141,6 @@ Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
    format "'[' 'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
-Notation "'exists' ! x , P" := 
-  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
-  (at level 200, x ident, right associativity,
-   format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" := 
-  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
-  (at level 200, x ident, right associativity,
-   format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
-
-
 (** Derived rules for universal quantification *)
 
 Section universal_quantification.
@@ -289,3 +279,14 @@ Proof.
 Qed.
 
 Hint Immediate sym_eq sym_not_eq: core v62.
+
+(** Other notations *)
+
+Notation "'exists' ! x , P" := 
+  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
+Notation "'exists' ! x : A , P" := 
+  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
-- 
cgit v1.2.3