diff options
| author | Vincent Laporte | 2019-04-24 11:48:46 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 09:51:05 +0000 |
| commit | 0e35f5f41b185309cbec3670ec8cfa8526e5fecf (patch) | |
| tree | 3c1571974112898b93523b1f026755f9dc0b97a0 /test-suite/output/Inductive.out | |
| parent | 2c18da20b260c55d8da49b1bb4f53e72dbc75a87 (diff) | |
Revert #8187
Diffstat (limited to 'test-suite/output/Inductive.out')
| -rw-r--r-- | test-suite/output/Inductive.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 2ba02924c9..af202ea01c 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)". + "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] |