blob: 05464755f0c911b9303d7a3e61cadc30a64f9c64 (
plain)
1
2
3
4
|
The command has indeed failed with message:
In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)",
"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
The term "I" has type "True" which should be Set, Prop or Type.
|
