+let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.index tree r (Utils.Right, equality) in
+ DT.index tree l (Utils.Left, equality)
+
+
+let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
+
+
+(* returns a list of all the equalities in the tree that are in relation
+ "mode" with the given term, where mode can be either Matching or
+ Unification.
+
+ Format of the return value: list of tuples in the form:
+ (position - Left or Right - of the term that matched the given one in this
+ equality,
+ equality found)
+
+ Note that if equality is "left = right", if the ordering is left > right,
+ the position will always be Left, and if the ordering is left < right,
+ position will be Right.
+*)