aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/bug5778.out
blob: 91ceb1b5837308b843ca6e1e3178de310f8bea2b (plain)
1
2
3
4
The command has indeed failed with message:
In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
failed.
The term "I" has type "True" which should be Set, Prop or Type.