diff options
| author | Pierre-Marie Pédrot | 2020-10-26 15:42:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-26 15:42:45 +0100 |
| commit | 42c1887379f3063e593910c569e3db8f227ac1b9 (patch) | |
| tree | 436a6ad1bb00c96f2a015c0b19b7786632090beb /kernel/type_errors.ml | |
| parent | 786f3b7d2d5cfdf3a5643192e5103863a8a04b1c (diff) | |
Adding a test for the second bug.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions