module SymbMap : Map.S with type key = B.t
- val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *)
- B.t Terms.unit_clause -> (* goal *)
+ val parse_symbols : B.t Terms.clause list -> (* hypotheses *)
+ B.t Terms.clause -> (* goal *)
(B.t * int * int * int * int list) list
- val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list
+ val dependencies : B.t -> B.t Terms.clause list -> B.t list
end