module Index (B : Orderings.Blob) :
sig
module ClauseSet : Set.S with
- type elt = Terms.direction * B.t Terms.unit_clause
+ type elt = Terms.direction * B.t Terms.clause
module FotermIndexable : Discrimination_tree.Indexable with
type constant_name = B.t and
type data = ClauseSet.elt and
type dataset = ClauseSet.t
- val index_unit_clause :
- DT.t -> B.t Terms.unit_clause -> DT.t
+ val index_clause :
+ DT.t -> B.t Terms.clause -> DT.t
- type active_set = B.t Terms.unit_clause list * DT.t
+ type active_set = B.t Terms.clause list * DT.t
end