diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Inductive.out | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index ff2556c5dc..e6c2806433 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,10 @@ 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". +In environment +list' : Set -> Set +A : Set +a : A +l : list' A +Unable to unify "list' (A * A)%type" with "list' A". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope |