File "./output/Errors.v", line 12, characters 0-11:
The command has indeed failed with message:
The field t is missing in Errors.M.
File "./output/Errors.v", line 19, characters 18-19:
The command has indeed failed with message:
Unable to unify "nat" with "True".
File "./output/Errors.v", line 20, characters 12-15:
The command has indeed failed with message:
Unable to unify "nat" with
"True".
In nested Ltac calls to "f" and "apply x", last call failed.
File "./output/Errors.v", line 29, characters 21-30:
The command has indeed failed with message:
Instance is not well-typed in the environment of ?x.
Ltac call to "instantiate ( (ident) := (lglob) )" failed.
File "./output/Errors.v", line 34, characters 19-20:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "?T -> nat" found for the type of f.
File "./output/Errors.v", line 35, characters 22-24:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "?T -> nat" found for the implicit
parameter A of id whose type is "Type".
File "./output/Errors.v", line 36, characters 17-18:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the
type of f in environment:
x : nat
File "./output/Errors.v", line 44, characters 5-23:
The command has indeed failed with message:
The first term has type "nat" while the second term has incompatible type
"bool".
File "./output/Errors.v", line 49, characters 7-24:
The command has indeed failed with message:
Replacement would lead to an ill-typed term: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"Set" : "Type"
"n" : "Type"
"n" : "Type"
The 2nd term has type "Type" which should be a subtype of
"Set". (universe inconsistency: Cannot enforce Errors.57 <= Set)
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
