;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
let meta_convertibility (pos,equality') =
Inference.meta_convertibility_eq equality equality'
in
;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
+ let _, _, (_, l, r, ordering), _ = equality in
let meta_convertibility (pos,equality') =
Inference.meta_convertibility_eq equality equality'
in