*** empty log message ***

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

3 files changed, 21 insertions, 21 deletions

diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 55d2dfb26f..d7120f89d5 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,5 +1,5 @@
 Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set :=
-      exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q)
+    exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q)
 (EX x:nat|x=x)
      : Prop
 [b:bool](if b then b else b)
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index c652a70281..3b40228861 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -30,25 +30,25 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
 
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
-Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
-  V8only (at level 200).
+Notation All := (all ?).
 Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
   V8only (at level 200, p at level 200).
-Notation All := (all ?).
+Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
+  V8only (at level 200).
 
-Notation "'EX' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
+Notation Ex  := (ex ?).
 Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation Ex  := (ex ?).
+Notation "'EX' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
+  V8only (at level 200, x at level 80).
 
-Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
-  (at level 10, p, q at level 8)
-  V8only "'EX2' x : t | p & q" (at level 200, x at level 80).
+Notation Ex2 := (ex2 ?).
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
   V8only "'EX2' x | p & q" (at level 200, x at level 80).
-Notation Ex2 := (ex2 ?).
+Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
+  (at level 10, p, q at level 8)
+  V8only "'EX2' x : t | p & q" (at level 200, x at level 80).
 
 (** Parsing only of things in [Logic.v] *)
 
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 08d4f47c5b..520e1971ff 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -19,25 +19,25 @@ Notation "x === y" := (identityT ? x y) (at level 5, no associativity)
 
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
-Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
+Notation AllT := (allT ?).
 Notation "'ALLT' x | p"     := (allT ? [x]p)   (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation AllT := (allT ?).
-
-Notation "'EXT' x : t | p"  := (exT t [x:t]p)  (at level 10, p at level 8)
+Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
+
+Notation ExT  := (exT ?).
 Notation "'EXT' x | p"      := (exT ? [x]p)    (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation ExT  := (exT ?).
+Notation "'EXT' x : t | p"  := (exT t [x:t]p)  (at level 10, p at level 8)
+  V8only (at level 200, x at level 80).
 
-Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q)
-  (at level 10, p, q at level 8)
-  V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
+Notation ExT2 := (exT2 ?).
 Notation "'EXT' x | p & q"     := (exT2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
   V8only "'EXT2' x | p & q" (at level 200, x at level 80).
-Notation ExT2 := (exT2 ?).
+Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q)
+  (at level 10, p, q at level 8)
+  V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
 
 (** Parsing only of things in [Logic_type.v] *)