summaryrefslogtreecommitdiff
path: root/test-suite/output/bug5778.out
blob: d6056c509854dd6caca8580a618a126eba8a415c (plain)
1
2
3
4
The command has indeed failed with message:
In nested Ltac calls to "c", "abs", "abstract b ltac:(())", 
"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.