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

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

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index beb3aed86da325f6369d99338237f53e0b9a0567..e44d79131db909a3e02697203cd7731bbf9925c5 100644 (file)
--- 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