diff options
| author | Maxime Dénès | 2013-12-22 04:03:40 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 16:52:26 -0400 |
| commit | 9b272a861bc3263c69b699cd2ac40ab2606543fa (patch) | |
| tree | cd56502b7bc95f22edcede303273c44bf0353f45 /lib/rtree.ml | |
| parent | ccd7546cd32c8a7901a4234f86aa23b4a7e1a043 (diff) | |
Tentative fix for the commutative cut subterm rule.
Some fixpoints are now rejected in the standard library, but that's probably
because we compare trees for equality instead of intersecting them.
Diffstat (limited to 'lib/rtree.ml')
0 files changed, 0 insertions, 0 deletions