aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-02-16 16:15:59 +0100
committerGaëtan Gilbert2018-02-16 16:18:14 +0100
commit4b7c0d2caad07f7d1199f37f86ae9830c09d81ca (patch)
tree0eaa583f56381a328cd2785d219ba4777db2f0e3 /kernel/cbytecodes.mli
parent507cd85244db835f13bc65cb9b92aa903180989c (diff)
Cleaner treatment of parameters in inferCumulativity
No using a mutable counter to skip them, instead we keep them in the environment.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions