aboutsummaryrefslogtreecommitdiff
path: root/lib/rtree.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-04-02 13:22:11 +0200
committerEmilio Jesus Gallego Arias2019-05-10 01:57:54 +0200
commit1cdaa823aa2db2f68cf63561a85771bb98aec70f (patch)
tree4359c3c1051797f89202793e788ee145a0826521 /lib/rtree.ml
parent8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (diff)
[api] Remove 8.10 deprecations.
Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it.
Diffstat (limited to 'lib/rtree.ml')
-rw-r--r--lib/rtree.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml
index e1c6a4c4d6..66d9eba3f7 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -115,8 +115,6 @@ struct
end
-let smartmap = Smart.map
-
(** Structural equality test, parametrized by an equality on elements *)
let rec raw_eq cmp t t' = match t, t' with
@@ -149,9 +147,6 @@ let equiv cmp cmp' =
let equal cmp t t' =
t == t' || raw_eq cmp t t' || equiv cmp cmp t t'
-(** Deprecated alias *)
-let eq_rtree = equal
-
(** Intersection of rtrees of same arity *)
let rec inter cmp interlbl def n histo t t' =
try