diff options
| author | Guillaume Melquiond | 2016-01-06 14:49:31 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-06 14:49:31 +0100 |
| commit | d0d46d9c5a93de25ecf0202a0ab3dbd83f1ed693 (patch) | |
| tree | 56e40e794519da0ad1d8d377907a9b39a9d2de2c /pretyping/typeclasses_errors.mli | |
| parent | 1afa595012bbaf5fb89398b355f16159e1af399b (diff) | |
Make code more readable by not mixing list traversal and option processing.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions