diff options
| author | Hugo Herbelin | 2018-06-29 12:13:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-29 02:40:22 +0200 |
| commit | a90aa1a2d7f0fd12621e744a67cc8c2abd24f9f8 (patch) | |
| tree | fdbfbc726e8652cf7524685cb1d24b5f5df71464 /kernel/type_errors.ml | |
| parent | bc480bb7068b0ffeeb8ad5cb90ee73fabc068d5f (diff) | |
Supporting locality flag for custom entries + compatibility with modules.
Also prevents to use an entry name already defined.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions