diff options
| author | Hugo Herbelin | 2020-08-19 14:57:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-25 22:27:31 +0200 |
| commit | 5d0c54e370ac20e9fbf249c3a7f1851a65e42acf (patch) | |
| tree | c443dae5ab8b2a207735fed5512f4c818b03a4e5 /dev/include | |
| parent | 324e647cb9372dff2c12088524d8371fa3c1cd85 (diff) | |
Moving production_level_eq to extend.ml for separation of concerns.
Add a mli file and uniformize indentation on the way.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions