+ module ClauseSet : Set.S with
+ type elt = Terms.direction * B.t Terms.unit_clause
+
+ module FotermIndexable : Discrimination_tree.Indexable with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm
+
+ module DT : Discrimination_tree.DiscriminationTree with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm and
+ type data = ClauseSet.elt and
+ type dataset = ClauseSet.t
+
+ val index_unit_clause :
+ DT.t -> B.t Terms.unit_clause -> DT.t