summaryrefslogtreecommitdiff
path: root/test-suite/output/Inductive.out
blob: e912003f035a6daaeb3a6bcd69dfe61ef074ccfb (plain)
1
2
3
The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
 "A -> list' A -> list' (A * A)%type".