end
*)
+
let string_of_discrimination_tree tree =
let rec to_string level = function
| DiscriminationTree.Node (value, map) ->
let index tree equality =
- let _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _, _ = equality in
let psl = path_string_of_term l
and psr = path_string_of_term r in
let index pos tree ps =
let remove_index tree equality =
- let _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _, _ = equality in
let psl = path_string_of_term l
and psr = path_string_of_term r in
let remove_index pos tree ps =
let in_index tree equality =
- let _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _, _ = equality in
let psl = path_string_of_term l
and psr = path_string_of_term r in
let meta_convertibility = Inference.meta_convertibility_eq equality in