X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=47119d4770e25beab157df62540aa120c0d1533e;hb=2041f4fefe300f77338f6aea598f025f84db1bbc;hp=306104658414913ece8eef01a984f462c86bb240;hpb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 306104658..47119d477 100644
--- 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