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

shows the polymorphism status of the term.

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index d1a6be9bd..5a3578f7d 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,11 +1,13 @@
 minus : nat -> nat -> nat
 
+minus is monomorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold minus avoiding to expose match constructs
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
+minus is monomorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold minus when applied to 1 argument
   avoiding to expose match constructs
@@ -13,6 +15,7 @@ minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
+minus is monomorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold minus
   when the 1st argument evaluates to a constructor and
@@ -21,6 +24,7 @@ minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
+minus is monomorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold minus when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
@@ -28,6 +32,7 @@ minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
+minus is monomorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold minus when the 1st and
   2nd arguments evaluate to a constructor 
@@ -37,6 +42,7 @@ pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
+pf is monomorphic
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -45,6 +51,7 @@ pf is transparent
 Expands to: Constant Top.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
+fcomp is monomorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
 The reduction tactics unfold fcomp when applied to 6 arguments 
@@ -52,17 +59,20 @@ fcomp is transparent
 Expands to: Constant Top.fcomp
 volatile : nat -> nat
 
+volatile is monomorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Top.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is monomorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is monomorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
@@ -70,6 +80,7 @@ f is transparent
 Expands to: Constant Top.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is monomorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
@@ -78,6 +89,7 @@ f is transparent
 Expands to: Constant Top.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is monomorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
@@ -86,6 +98,7 @@ f is transparent
 Expands to: Constant Top.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is monomorphic
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent