diff options
| author | Maxime Dénès | 2020-02-12 10:27:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:42 +0200 |
| commit | c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 (patch) | |
| tree | 9ebe8a6c3959c670a9cff263cfa6d08f196bbc99 /test-suite/output | |
| parent | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (diff) | |
Remove special case for implicit inductive parameters
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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 |