diff options
| author | Maxime Dénès | 2018-04-14 21:57:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-14 21:59:15 +0200 |
| commit | ab2e6772c6cbe2e6fa8851a1b399222a2a7740e3 (patch) | |
| tree | 8bd8a4bd811af8a57f7b675741221a5a9c849511 /kernel/type_errors.ml | |
| parent | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (diff) | |
[Sphinx] Fix all remaining warnings.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions