diff options
| author | Arnaud Spiwack | 2014-02-25 12:32:34 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-25 17:13:45 +0100 |
| commit | f931b170b3be3da2e2c245c566aad2b483223a51 (patch) | |
| tree | 530aa41e9827f30a01248820d0eef577901470de /kernel/type_errors.mli | |
| parent | d35a5022f45f1082c83891a6d0af32485a9db7d6 (diff) | |
Tacinterp: remove unnecessary return/bind pairs.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions