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

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index beb3aed86..e44d79131 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -13,6 +13,7 @@
 
 module Index(B : Orderings.Blob) = struct
   module U = FoUtils.Utils(B)
+  module Clauses = Clauses.Clauses(B)
 
   module ClauseOT =
     struct 
@@ -23,7 +24,7 @@ module Index(B : Orderings.Blob) = struct
  
       let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = 
         let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
-        if c <> 0 then c else U.compare_clause uc1 uc2
+        if c <> 0 then c else Clauses.compare_clause uc1 uc2
       ;;
     end