diff options
| author | Maxime Dénès | 2019-04-25 10:44:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:30:34 +0200 |
| commit | afb58502f900554986aeee9a749871630f117edd (patch) | |
| tree | a40e9d81fac3f3a4474ce8d1f201154f6b44536f /kernel/type_errors.ml | |
| parent | 321d26480444c947ffdaaf849157fd373e40c988 (diff) | |
Test case for #5752
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions