summaryrefslogtreecommitdiff
path: root/test-suite/output/Arguments.out
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/output/Arguments.out
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/output/Arguments.out')
-rw-r--r--test-suite/output/Arguments.out88
1 files changed, 52 insertions, 36 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 7c9b1e27..629a1ab6 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,94 +1,110 @@
-minus : nat -> nat -> nat
+Nat.sub : nat -> nat -> nat
+Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+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 simpl tactic unfolds minus when applied to 1 argument
- avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+The reduction tactics unfold Nat.sub when applied to 1 argument
+ 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 simpl tactic unfolds minus
+The reduction tactics unfold Nat.sub
when the 1st argument evaluates to a constructor and
- when applied to 1 argument avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+ when applied to 1 argument 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 simpl tactic unfolds minus
- when the 1st and 2nd arguments evaluate to a constructor and
- when applied to 2 arguments
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+The reduction tactics unfold Nat.sub when the 1st and
+ 2nd arguments evaluate to a constructor and when applied to 2 arguments
+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 simpl tactic unfolds minus
- when the 1st and 2nd arguments evaluate to a constructor
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
+The reduction tactics unfold Nat.sub when the 1st and
+ 2nd arguments evaluate to a constructor
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
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 _ _ _ _ _]
-The simpl tactic never unfolds pf
+The reduction tactics never unfold pf
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 simpl tactic unfolds fcomp when applied to 6 arguments
+The reduction tactics unfold fcomp when applied to 6 arguments
fcomp is transparent
Expands to: Constant Top.fcomp
volatile : nat -> nat
+volatile is not universe polymorphic
Argument scope is [nat_scope]
-The simpl tactic always unfolds volatile
+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 simpl tactic unfolds f
- when the 3rd, 4th and 5th arguments evaluate to a constructor
+The reduction tactics unfold f when the 3rd, 4th and
+ 5th arguments evaluate to a constructor
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 simpl tactic unfolds f
- when the 4th, 5th and 6th arguments evaluate to a constructor
+The reduction tactics unfold f when the 4th, 5th and
+ 6th arguments evaluate to a constructor
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 simpl tactic unfolds f
- when the 5th, 6th and 7th arguments evaluate to a constructor
+The reduction tactics unfold f when the 5th, 6th and
+ 7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.f
+ = forall v : unit, f 0 0 5 v 3 = 2
+ : Prop
+ = 2 = 2
+ : Prop
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
-The simpl tactic unfolds f
- when the 5th, 6th and 7th arguments evaluate to a constructor
+f is not universe polymorphic
+The reduction tactics unfold f when the 5th, 6th and
+ 7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.f
forall w : r, w 3 true = tt