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