val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
- val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int
+ val fresh_clause : int ->
+ ?subst: B.t Terms.substitution ->
+ B.t Terms.clause -> B.t Terms.clause * int
val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list
-> B.t Terms.foterm -> B.t Terms.clause * int
val are_alpha_eq_cl :
B.t Terms.clause -> B.t Terms.clause -> bool
+ val vars_of_clause :
+ B.t Terms.clause -> int list
+
+ (*val apply_subst :
+ B.t Terms.substitution -> B.t Terms.clause -> B.t Terms.clause*)
+
end