diff options
| author | Hugo Herbelin | 2014-10-20 12:51:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-20 23:36:57 +0200 |
| commit | 98f3abb83a26b85092140e8850fd372622f24bdb (patch) | |
| tree | 2c189219d24fe629d95cd27d63a1da543f7d6341 /dev/header | |
| parent | 7efeff178470ab204e531cd07176091bf5022da6 (diff) | |
Fixing a (new) part of bug #2729.
By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.
This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.
Another part is still open (see test-suite).
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions