-
Notifications
You must be signed in to change notification settings - Fork 1
/
Errors.out
19 lines (19 loc) · 887 Bytes
/
Errors.out
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
The command has indeed failed with message:
The field t is missing in Errors.M.
The command has indeed failed with message:
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.
Unable to unify "nat" with "True".
The command has indeed failed with message:
Ltac call to "instantiate ( (ident) := (lglob) )" failed.
Instance is not well-typed in the environment of ?x.
The command has indeed failed with message:
Cannot infer ?T in the partial instance "?T -> nat" found for the type of f.
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".
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