blob: 25a306b4582b97def3d356a7ef747ad22ee0f42b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
The command has indeed failed with message:
Cannot coerce to a disjunctive/conjunctive pattern.
The command has indeed failed with message:
Disjunctive/conjunctive introduction pattern expected.
The command has indeed failed with message:
Cannot coerce to a disjunctive/conjunctive pattern.
The command has indeed failed with message:
Cannot coerce to a disjunctive/conjunctive pattern.
The command has indeed failed with message:
Ltac variable H is bound to <tactic closure> which cannot be coerced to
an introduction pattern.
The command has indeed failed with message:
Disjunctive/conjunctive introduction pattern expected.
The command has indeed failed with message:
Ltac variable H' is bound to <tactic closure> which cannot be coerced to
an introduction pattern.
|
