diff options
| author | Gaëtan Gilbert | 2018-11-14 15:26:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-23 13:21:59 +0100 |
| commit | 8a9d0ab4b5469f3042f4dbd32e7fde3294b5e8de (patch) | |
| tree | 06f6115d40ae45554983a9879b694fa08895334b /kernel/indtypes.ml | |
| parent | 8fb01564fba587142c2471708ff18219f1c64903 (diff) | |
Fix #8937: inductive conversion in coqchk subtyping
As far as I can tell this is similar to what coqtop does. Delta
resolvers are complicated so I may be mistaken.
The important part is to avoid losing the modified delta resolver
returned by strengthen_and_subst in check_mexpr.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions