Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 0 insertions, 9 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index d5903483..09f032d4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,8 +6,6 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
-t_rect is not universe polymorphic
      = fun d : TT => match d with
                      | @CTT _ _ b => b
                      end
@@ -26,7 +24,6 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-uncast is not universe polymorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
-
-foo' is not universe polymorphic
 f = 
 fun H : B =>
 match H with
@@ -61,5 +54,3 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
-
-f is not universe polymorphic