mise a jour nouvelle syntaxe

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

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 6abbfa9f87..469a9d4bf6 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -123,28 +123,28 @@ Definition all := [A:Type][P:A->Prop](x:A)(P x).
 V7only [ Notation Ex  := (ex ?). ].
 Notation "'EX' x | p"      := (ex ? [x]p)
   (at level 10, p at level 8) : type_scope
-  V8only (at level 200, x ident, p at level 80).
+  V8only "'exists' x | p" (at level 200, x ident, p at level 80).
 Notation "'EX' x : t | p"  := (ex ? [x:t]p)
   (at level 10, p at level 8) : type_scope
-  V8only (at level 200, x ident, p at level 80).
+  V8only "'exists' x : t | p" (at level 200, x ident, p at level 80).
 
 V7only [ Notation Ex2 := (ex2 ?). ].
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8) : type_scope
-  V8only "'EX2' x | p & q" (at level 200, x ident, p, q at level 80).
+  V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 80).
 Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8) : type_scope
-  V8only "'EX2' x : t | p & q"
+  V8only "'exists2' x : t | p & q"
     (at level 200, x ident, t at level 200, p, q at level 80).
 
-V7only [Notation All := (all ?).].
+V7only [Notation All := (all ?).
 Notation "'ALL' x | p"     := (all ? [x]p)
   (at level 10, p at level 8) : type_scope
   V8only (at level 200, x ident, p at level 200).
 Notation "'ALL' x : t | p" := (all ? [x:t]p)
   (at level 10, p at level 8) : type_scope
   V8only (at level 200, x ident, t, p at level 200).
-
+].
 
 (** Universal quantification *)