diff options
| author | Matej Kosik | 2015-11-24 18:12:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:20 +0100 |
| commit | 9e12f35ddf03dd47af99284fa9bfbb14759834b8 (patch) | |
| tree | 500e5917a0f5636e1d326888aec0491ccfc5d5d0 /kernel/type_errors.ml | |
| parent | f43f474fe3ba0b01115ef02b0032f706879ee521 (diff) | |
ENH: redundant examples were removed
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions