diff options
| author | Gaëtan Gilbert | 2020-02-07 15:18:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 15:18:39 +0100 |
| commit | 51c0b1414be9a46e221b13f652474db0194093fc (patch) | |
| tree | 8b260deab34b79ee2a251f65e9de75c2b292dd36 /kernel/type_errors.mli | |
| parent | e2d25ea2b9df57ba4006cbc9c04b8f0dfbd2733a (diff) | |
Remove confusing commented code in funind
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions