aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Arguments.out13
-rw-r--r--test-suite/output/ArgumentsScope.out14
-rw-r--r--test-suite/output/Arguments_renaming.out7
-rw-r--r--test-suite/output/Cases.out9
-rw-r--r--test-suite/output/Errors.out2
-rw-r--r--test-suite/output/Implicit.out1
-rw-r--r--test-suite/output/PrintInfos.out10
-rw-r--r--test-suite/output/TranspModtype.out8
-rw-r--r--test-suite/output/inference.out2
9 files changed, 65 insertions, 1 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
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 6643c1429..358a96bc3 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,56 +1,70 @@
a : bool -> bool
+a is monomorphic
Argument scope is [bool_scope]
Expands to: Variable a
b : bool -> bool
+b is monomorphic
Argument scope is [bool_scope]
Expands to: Variable b
negb'' : bool -> bool
+negb'' is monomorphic
Argument scope is [bool_scope]
negb'' is transparent
Expands to: Constant Top.A.B.negb''
negb' : bool -> bool
+negb' is monomorphic
Argument scope is [bool_scope]
negb' is transparent
Expands to: Constant Top.A.negb'
negb : bool -> bool
+negb is monomorphic
Argument scope is [bool_scope]
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
a : bool -> bool
+a is monomorphic
Expands to: Variable a
b : bool -> bool
+b is monomorphic
Expands to: Variable b
negb : bool -> bool
+negb is monomorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool
+negb' is monomorphic
negb' is transparent
Expands to: Constant Top.A.negb'
negb'' : bool -> bool
+negb'' is monomorphic
negb'' is transparent
Expands to: Constant Top.A.B.negb''
a : bool -> bool
+a is monomorphic
Expands to: Variable a
negb : bool -> bool
+negb is monomorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool
+negb' is monomorphic
negb' is transparent
Expands to: Constant Top.negb'
negb'' : bool -> bool
+negb'' is monomorphic
negb'' is transparent
Expands to: Constant Top.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 695efb260..c440d5ba7 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -20,6 +20,7 @@ For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
+eq_refl is monomorphic
Arguments are renamed to B, y
When applied to no arguments:
Arguments B, y are implicit and maximally inserted
@@ -35,6 +36,7 @@ For myEq: Argument scopes are [type_scope _ _]
For myrefl: Argument scopes are [type_scope _ _]
myrefl : forall (B : Type) (x : A), B -> myEq B x x
+myrefl is monomorphic
Arguments are renamed to C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope _ _]
@@ -47,11 +49,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
+myplus is monomorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
+myplus is monomorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -70,6 +74,7 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
For myrefl: Argument scopes are [type_scope type_scope _ _]
myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
+myrefl is monomorphic
Arguments are renamed to A, C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope type_scope _ _]
@@ -84,11 +89,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
+myplus is monomorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
+myplus is monomorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
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
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 839611b65..bcc37b635 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -4,4 +4,4 @@ The command has indeed failed with message:
=> Error: Unable to unify "nat" with "True".
The command has indeed failed with message:
=> In nested Ltac calls to "f" and "apply x", last call failed.
- Error: Unable to unify "nat" with "True".
+Error: Unable to unify "nat" with "True".
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c2..d1cd5e84f 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,6 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
+d2 is monomorphic
Arguments x, x0 are implicit
Argument scopes are [nat_scope nat_scope _]
map id (1 :: nil)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index e0fb7d5a9..62889f802 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,5 +1,6 @@
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
+existT is template universe polymorphic
Argument A is implicit
Argument scopes are [type_scope _ _ _]
Expands to: Constructor Coq.Init.Specif.existT
@@ -24,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
+eq_refl is monomorphic
When applied to no arguments:
Arguments A, x are implicit and maximally inserted
When applied to 1 argument:
@@ -44,9 +46,11 @@ fix plus (n m : nat) {struct n} : nat :=
end
: nat -> nat -> nat
+plus is monomorphic
Argument scopes are [nat_scope nat_scope]
plus : nat -> nat -> nat
+plus is monomorphic
Argument scopes are [nat_scope nat_scope]
plus is transparent
Expands to: Constant Coq.Init.Peano.plus
@@ -54,6 +58,7 @@ plus : nat -> nat -> nat
plus_n_O : forall n : nat, n = n + 0
+plus_n_O is monomorphic
Argument scope is [nat_scope]
plus_n_O is opaque
Expands to: Constant Coq.Init.Peano.plus_n_O
@@ -75,11 +80,13 @@ For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
comparison : Set
+comparison is monomorphic
Expands to: Inductive Coq.Init.Datatypes.comparison
Inductive comparison : Set :=
Eq : comparison | Lt : comparison | Gt : comparison
bar : foo
+bar is monomorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
@@ -87,12 +94,14 @@ Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
+bar is monomorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
bar : foo
+bar is monomorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
@@ -100,6 +109,7 @@ Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
+bar is monomorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f94ed6423..dbbd73dcd 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,15 @@
TrM.A = M.A
: Set
+
+TrM.A is monomorphic
OpM.A = M.A
: Set
+
+OpM.A is monomorphic
TrM.B = M.B
: Set
+
+TrM.B is monomorphic
*** [ OpM.B : Set ]
+
+OpM.B is monomorphic
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index a394c56dd..466faaccb 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,6 +4,8 @@ fun e : option L => match e with
| None => None
end
: option L -> option L
+
+P is monomorphic
fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
: forall m n p : nat, S m <= S n + p -> m <= n + p
fun n : nat => let x := A n in ?12 ?15:T n
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:05:17 +0000