(* $Id$ *)
-module Index (B : Terms.Blob) :
+module Index (B : Orderings.Blob) :
sig
module ClauseSet : Set.S with
type elt = Terms.direction * B.t Terms.unit_clause
type input = B.t Terms.foterm and
type data = ClauseSet.elt and
type dataset = ClauseSet.t
+
+ val index_unit_clause :
+ int -> DT.t -> B.t Terms.unit_clause -> DT.t
+
+ type active_set = B.t Terms.unit_clause list * DT.t
end