diff options
| author | Pierre-Marie Pédrot | 2016-02-19 13:59:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-19 14:08:29 +0100 |
| commit | d3012c8ac308b18272ddaa90c4eae7e517b63c7c (patch) | |
| tree | 638f2414200a51bfe7eb1b8a0888c0f2d250f24a /kernel/type_errors.mli | |
| parent | 9aa2d99fb1ad6b348142fce244f277b9dd25017f (diff) | |
Fixing bug #4582: cannot override notation [ x ].
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions