diff options
| author | Emilio Jesus Gallego Arias | 2019-04-29 20:10:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-29 20:10:54 +0200 |
| commit | 75dc5da6ceefb30bd741971f303c95d3af1622de (patch) | |
| tree | c2e08253cd65f59e81fd0bdb9ee8693f7cf063ff /test-suite/output/Inductive.out | |
| parent | 61a1b4c46e4584e9337f9298b5f0053858a03c93 (diff) | |
| parent | a3c03857991f3f0d84edb109aaa68a03753699a6 (diff) | |
Merge PR #9987: Fix #9180 by reverting #9249 and #8187
Reviewed-by: maximedenes
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 _] |