diff options
| author | Pierre-Marie Pédrot | 2018-10-02 08:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 08:18:34 +0200 |
| commit | 0579efd93eebb18f94c90718b092ae4b68a2262d (patch) | |
| tree | 67b0c04e088a8fc1150b6850ecca5efafa2b1b19 /kernel/type_errors.mli | |
| parent | ccb701d78394a108daf25e62d40ba059aa3fce62 (diff) | |
Fix deprecation warnings.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions