diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-12 17:44:29 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:20 +0200 |
| commit | 5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f (patch) | |
| tree | 9c71c3f6b678ccbfdcb882fc6a951ad303f7850a /checker/cic.mli | |
| parent | ab0c49baa8d57ed92a79e7d0b0737267042210f8 (diff) | |
use map_constr more efficiently
Diffstat (limited to 'checker/cic.mli')
0 files changed, 0 insertions, 0 deletions