MAJ avec les particularités de l'afficheur v7 de la V8

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

5 files changed, 25 insertions, 16 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 5f13caafc4..a35885651f 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -1,4 +1,6 @@
 t_rect = 
-[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))]
- Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end}
-     : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t)
+[P:(t ->Type); f:([x:=t](x0:x)(P x0) ->(P (k x0)))]
+ Fix F
+   {F [t:t] : (P t) := <[t0:t](P t0)>Cases t of (k x x0) => (f x0 (F x0)) end}
+     : (P:(t ->Type))([x:=t](x0:x)(P x0) ->(P (k x0))) ->(t:t)(P t)
+
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index f9cf9efcb4..f5c812c8a7 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -1,5 +1,10 @@
+(compose 3!nat S)
+     : (nat ->nat) ->nat ->nat
+(ex_intro 2![_:nat]True 3!(0) I)
+     : (ex [_:nat]True)
 d2 = [x:nat](d1 1!x)
      : (x,x0:nat)x0=x ->x0=x
 
+
 Positions [1; 2] are implicit
 Argument scopes are [nat_scope nat_scope _]
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index d7120f89d5..79ddf8c447 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,6 +1,8 @@
-Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set :=
-    exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q)
+Inductive sig2 [A : Set; P : A ->Prop; Q : A ->Prop] : Set :=
+    exist2 : (x:A)(P x) ->(Q x) ->(sig2 A P Q)
+For sig2: Argument scopes are [type_scope type_scope type_scope]
+For exist2: Argument scopes are [type_scope _ _ _ _ _]
 (EX x:nat|x=x)
      : Prop
 [b:bool](if b then b else b)
-     : bool->bool
+     : bool ->bool
diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out
index 22422602e8..e8b215bc75 100644
--- a/test-suite/output/Sum.out
+++ b/test-suite/output/Sum.out
@@ -1,4 +1,4 @@
-nat+nat+{True}
+'type:nat+nat '+{True}
      : Set
 {True}+{True}+{True}
      : Set
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index 0fdc5b7e39..e856686ac3 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -1,21 +1,21 @@
 `32`
      : Z
-[f:(nat->Z)]`(f O)+0`
-     : (nat->Z)->Z
+[f:(nat ->Z)]`(f O)+0`
+     : (nat ->Z) ->Z
 [x:positive](POS (xO x))
-     : positive->Z
+     : positive ->Z
 [x:positive]`(POS x)+1`
-     : positive->Z
+     : positive ->Z
 [x:positive](POS x)
-     : positive->Z
+     : positive ->Z
 [x:positive](NEG (xO x))
-     : positive->Z
+     : positive ->Z
 [x:positive]`(POS (xO x))+0`
-     : positive->Z
+     : positive ->Z
 [x:positive]`(Zopp (POS (xO x)))`
-     : positive->Z
+     : positive ->Z
 [x:positive]`(Zopp (POS (xO x)))+0`
-     : positive->Z
+     : positive ->Z
 `(inject_nat (0))+1`
      : Z
 `0+(inject_nat (plus (0) (0)))`