diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-05 14:05:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-05 14:05:04 +0200 |
| commit | 7399d4b3da04e0464b0c47f6c0b3c948599f6873 (patch) | |
| tree | b9b94ddef8481d48c5be77dc7a5dd96972d1eccd /kernel/subtyping.mli | |
| parent | 8c3455e2f5db09e70cd7a40a96856f5be79adaff (diff) | |
Test for bug #3142, actually duplicate of #3262.
Diffstat (limited to 'kernel/subtyping.mli')
0 files changed, 0 insertions, 0 deletions