-*)
-
- let remove_index tree term info =
- let ps = path_string_of_term term in
- try
- let ps_set =
- A.remove info (DiscriminationTree.find ps tree) in
- if A.is_empty ps_set then
- DiscriminationTree.remove ps tree
- else
- DiscriminationTree.add ps ps_set tree
- with Not_found ->
- tree
-
-(*
-let remove_index tree equality =
- 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 =
- try
- let ps_set =
- PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in
- if PosEqSet.is_empty ps_set then
- DiscriminationTree.remove ps tree
- else
- DiscriminationTree.add ps ps_set tree
- with Not_found ->
- tree
- in
- match ordering with
- | Utils.Gt -> remove_index Utils.Left tree psl
- | Utils.Lt -> remove_index Utils.Right tree psr
- | _ ->
- let tree = remove_index Utils.Left tree psl in
- remove_index Utils.Right tree psr
-;;
-*)
-
-
- let in_index tree term test =
- let ps = path_string_of_term term in
- try
- let ps_set = DiscriminationTree.find ps tree in
- A.exists test ps_set
- with Not_found ->
- false
-
-(*
- let in_index tree equality =
- 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
- let ok ps =
- try
- let set = DiscriminationTree.find ps tree in
- PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
- with Not_found ->
- false
- in
- (ok psl) || (ok psr)
-;;
-*)