Fixing output test-suite: since universe polymorphism, the Print command

shows the polymorphism status of the term.

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index be1bff48b..6515b368d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ 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 monomorphic
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match eq_nat_dec x y with
@@ -16,6 +18,7 @@ match eq_nat_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
+proj is monomorphic
 Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -26,6 +29,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
+foo is monomorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -33,9 +37,12 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
+uncast is monomorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
+
+foo' is monomorphic
 f = 
 fun H : B =>
 match H with
@@ -46,3 +53,5 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+
+f is monomorphic