diff options
| author | Maxime Dénès | 2014-03-14 18:17:06 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 17:55:06 -0400 |
| commit | 3077bf499e88754196b42b7241abe8153544cc40 (patch) | |
| tree | d453e1be9c28630af1433f76dbf3d7b1ffb36f92 /kernel/type_errors.ml | |
| parent | 7b22ae388286564c008e6cd618b3546a03060107 (diff) | |
Simplified rect2, it turns out Arthur's trick was not required.
Standard library now compiles fully.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions