diff options
| author | Pierre Courtieu | 2015-01-15 16:34:01 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-01-15 16:34:01 +0100 |
| commit | 62ce6ac2a237917d9f75f78439898787a27829ad (patch) | |
| tree | 5c4ef95a7cf2b7c4c7ff91e818485e021aa9db7e /kernel/type_errors.mli | |
| parent | 6eab6444ddf9d7de820602ceff8b285e28619cce (diff) | |
Added stuff about -I -Q -R in COMPATIBILTY.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions