Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib...

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 306104658414913ece8eef01a984f462c86bb240..47119d4770e25beab157df62540aa120c0d1533e 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -14,11 +14,12 @@
 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
 
@@ -688,7 +689,7 @@ module Superposition (B : Orderings.Blob) =
         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