diff options
| author | Hugo Herbelin | 2017-09-23 13:39:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-23 13:53:28 +0200 |
| commit | 6d1b7368267a4da980980efa682cf3fb8f1e8394 (patch) | |
| tree | 30f6a854282e956adcc192bab33650a3fdf66502 /kernel/type_errors.mli | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
Fixing _rect bug for inductive types with let-ins and non-rec uniform params.
The bug was caused by an inconsistency in different part of the code
for deciding where cutting the context in between recursively uniform
parameters and non-recursively uniform ones when let-ins were in the
middle. We fix it by using uniformly "context_chop".
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions