diff options
| author | Vincent Laporte | 2018-09-06 17:28:38 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-06 17:28:38 +0200 |
| commit | f6ed48098636f11362945d380bbe8cb71a9ab2ee (patch) | |
| tree | fdc69b612c5160aac16e8fdc09c5fb67991bd5af /kernel/type_errors.mli | |
| parent | 1877e1235c63ff3bbc958e5a79fa052ac852071c (diff) | |
Deprecation warning in legacy tacextend.mlp
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions