module Superposition (B : Orderings.Blob) =
struct
module IDX = Index.Index(B)
- module Unif = FoUnif.Founif(B)
+ module Unif = FoUnif.FoUnif(B)
module Subst = FoSubst
module Order = B
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
+ module Clauses = Clauses.Clauses(B)
exception Success of B.t Terms.bag * int * B.t Terms.clause
current :: alist, IDX.index_clause atable current
in
debug (lazy "Indexed");
- let fresh_current, maxvar = Utils.fresh_clause maxvar current in
+ let fresh_current, maxvar = Clauses.fresh_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
let bag, fresh_current = Terms.add_to_bag fresh_current bag in