diff options
| author | Hugo Herbelin | 2015-10-22 22:25:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-22 22:37:44 +0200 |
| commit | 273005ac85e9ae0c23328e243edeadfc8dcaf8bb (patch) | |
| tree | 4084d81a08d34d541122fb3fc91574bce1003ba5 /test-suite/output/Inductive.out | |
| parent | 95b04506542064fbda7a61c4b6ce276a668d25bd (diff) | |
Fixing a bug in reporting ill-formed inductive.
Was introduced in b06d3badb (15 Jul 2015).
Diffstat (limited to 'test-suite/output/Inductive.out')
| -rw-r--r-- | test-suite/output/Inductive.out | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out new file mode 100644 index 0000000000..e912003f03 --- /dev/null +++ b/test-suite/output/Inductive.out @@ -0,0 +1,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". |