diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-09 08:26:00 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-09 08:26:00 +0100 |
commit | e4ad47fed594d6865f5bd29a159976cb072f0fae (patch) | |
tree | 893bd81fe7df422d7c0a2bd545650a1e7ca86268 /test-suite/output/Arguments.out | |
parent | d337afac6f9b1fe405c89b4e62f660cadf171f0f (diff) |
Do not display the status of monomorphic constants unless in universe-polymorphism mode.
Diffstat (limited to 'test-suite/output/Arguments.out')
-rw-r--r-- | test-suite/output/Arguments.out | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 9c488ce5a..2c7b04c62 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,13 +1,11 @@ Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs @@ -15,7 +13,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and @@ -24,7 +21,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments @@ -32,7 +28,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor @@ -42,7 +37,6 @@ pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 -pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] @@ -51,7 +45,6 @@ pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C -fcomp is not universe polymorphic 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 @@ -59,20 +52,17 @@ fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat -volatile is not universe polymorphic 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 not universe polymorphic 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 not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor @@ -80,7 +70,6 @@ f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and @@ -89,7 +78,6 @@ f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic 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 @@ -102,7 +90,6 @@ Expands to: Constant Top.f : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent |