diff options
| author | Ismail | 2017-12-27 19:21:02 +0000 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-08 11:12:34 +0100 |
| commit | 8957279df5d927334695aee64caf4f6af37f828d (patch) | |
| tree | e3c10919265d3eb29de2627e310b4228853226ca /kernel/type_errors.mli | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
Document between and exists_between types.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions