aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-09-28 15:38:33 +0200
committerGuillaume Melquiond2016-10-22 11:57:58 +0200
commit80d5779409bf33fbe5043275b96775a5f04a3b2c (patch)
tree7e38bd03ccf57a9c24971441bfa57d0a792edfbe /kernel/cbytecodes.ml
parentcc2778c3310a75585c00f0eb659ddde7aee2944a (diff)
Remove incorrect assertion in cbn (bug #4822).
This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion).
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions