diff options
| author | Pierre Courtieu | 2015-10-19 11:49:38 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2015-10-19 11:49:38 +0200 |
| commit | 70d3ad33f6ba7a1c6b1fb93aadd5c05d7e9c03b8 (patch) | |
| tree | 3f26ad08ebf92d5ed69500ad514ba7e4cc748f59 /kernel/type_errors.ml | |
| parent | de32427bd2785c365374c554b4b74e97749cb995 (diff) | |
Partly fixes #3225. Removed some old experimental stuff in funind.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions