diff options
| author | Hugo Herbelin | 2015-11-06 17:37:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-10 14:36:14 +0100 |
| commit | bde12b7066d7d1f3849d529428b2be3343a27787 (patch) | |
| tree | 8f96bf29f331bc7d361ed7965af996f23d122d3e /dev | |
| parent | 5587499e721f4aa1f2cf35596a8f7aa58d852592 (diff) | |
Fixing a bug in reporting ill-formed constructor.
For instance,
Inductive a (x:=1) := C : a -> True.
was wrongly reporting
Error: The type of constructor C
is not valid; its conclusion must be
"a" applied to its parameter.
Also "simplifying" explain_ind_err.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions