diff options
| author | Matthieu Sozeau | 2014-07-14 19:16:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-14 19:18:42 +0200 |
| commit | 7319524e236545c1b7b799950babbb4886415360 (patch) | |
| tree | 4cc3f708205d0e4bb20c1443175ef83f3421f79d /kernel/type_errors.ml | |
| parent | 7f73c09a6031578a1531fade2752b6e99655cba0 (diff) | |
Add interface function to replace new_Type ()
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions