diff options
| author | Maxime Dénès | 2016-07-18 11:30:39 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-18 11:30:39 +0200 |
| commit | 2042daa9a6e13cbb9636a62812015749d95c2283 (patch) | |
| tree | cbf6e5015eee1ed9ad6792d837dcc63423dee3fd /kernel/type_errors.mli | |
| parent | 8c7ecc85f5535e9d409d51087b1119fe1e61f0cb (diff) | |
Replacing deprecated Implicit Arguments in prelude.
Was triggering a deprecation warning.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions