Update test-suite output

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

2 files changed, 6 insertions, 8 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 9d0d06580..995754a6b 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -21,7 +21,7 @@ Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
-  | nil => None (A:=A)
+  | nil => None
   | x0 :: nil => Some x0
   | x0 :: (_ :: _) as l0 => foo A l0
   end
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index f4270d3de..8bc855216 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,6 +1,6 @@
 fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
 list B := match l with
-          | nil => nil (A:=B)
+          | nil => nil
           | a :: l0 => f a :: F A B f l0
           end
      : forall A B : Set, (A -> B) -> list A -> list B
@@ -14,12 +14,10 @@ fix even_pos_odd_pos 2
  intros.
  destruct H.
    omega.
-  
    apply odd_pos_even_pos in H.
    omega.
+  intros.
+  destruct H.
+   apply even_pos_odd_pos in H.
+   omega.
   
- intros.
- destruct H.
-  apply even_pos_odd_pos in H.
-  omega.
-