aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorHugo Herbelin2017-09-23 13:39:48 +0200
committerHugo Herbelin2017-09-23 13:53:28 +0200
commit6d1b7368267a4da980980efa682cf3fb8f1e8394 (patch)
tree30f6a854282e956adcc192bab33650a3fdf66502 /kernel/cbytecodes.ml
parent06a723190858da8ed3f30736f22398aa7822c959 (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/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions