diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-16 16:15:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-16 16:18:14 +0100 |
| commit | 4b7c0d2caad07f7d1199f37f86ae9830c09d81ca (patch) | |
| tree | 0eaa583f56381a328cd2785d219ba4777db2f0e3 /printing/printmod.mli | |
| parent | 507cd85244db835f13bc65cb9b92aa903180989c (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 'printing/printmod.mli')
0 files changed, 0 insertions, 0 deletions