aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/rtree.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2013-12-22 04:03:40 -0500
committerGravatar Maxime Dénès <mail@maximedenes.fr>2014-07-22 16:52:26 -0400
commit9b272a861bc3263c69b699cd2ac40ab2606543fa (patch)
treecd56502b7bc95f22edcede303273c44bf0353f45 /lib/rtree.ml
parentccd7546cd32c8a7901a4234f86aa23b4a7e1a043 (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