diff options
| author | Maxime Dénès | 2018-07-20 18:01:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 14:42:45 +0200 |
| commit | f54192a50eaf14852e1462f24e4168aa8a8545fe (patch) | |
| tree | 64696d9c111f420e9bff7d7f742602a6b38f8b0a /kernel/type_errors.mli | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions