aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorHugo Herbelin2017-07-26 22:34:43 +0200
committerHugo Herbelin2017-08-21 13:14:43 +0200
commitdd56ef10395a2ced84612aa799690b034306806e (patch)
treee6fe2bc49b5154c5f6ee8f951a900905f4260af0 /kernel/cbytecodes.ml
parent9490c6099e1da94fcf315aba48125993cd180327 (diff)
Fixing another regression with 8.4 wrt to βι-normalization of created hyps.
This one is a continuation of e2a8edaf59 which was βι-normalizing the hypotheses created by a "match". We forgot to do it for "let" and "if". This is what this commit is doing.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions