X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Findex.ml;h=fa5d86ee3e913cf14409b13e6c82bfbbc86c13d6;hb=6b76c5b3b82753966cabffd8536d8dd9f8cada20;hp=c1e12a34dbbc684c38560e2bae7ff046aff1eabf;hpb=aa5c8c99c9f7ae285883cff133fc02b3d064888c;p=helm.git

diff --git a/matita/components/ng_paramodulation/index.ml b/matita/components/ng_paramodulation/index.ml
index c1e12a34d..fa5d86ee3 100644
--- a/matita/components/ng_paramodulation/index.ml
+++ b/matita/components/ng_paramodulation/index.ml
@@ -21,7 +21,7 @@ module Index(B : Orderings.Blob) = struct
       type t = Terms.direction * B.t Terms.unit_clause
  
       let compare (d1,uc1) (d2,uc2) = 
-        let c = Pervasives.compare d1 d2 in
+        let c = Stdlib.compare d1 d2 in
         if c <> 0 then c else U.compare_unit_clause uc1 uc2
       ;;
     end
@@ -61,7 +61,7 @@ module Index(B : Orderings.Blob) = struct
         match e1,e2 with 
         | Constant (a1,ar1), Constant (a2,ar2) ->
             let c = B.compare a1 a2 in
-            if c <> 0 then c else Pervasives.compare ar1 ar2
+            if c <> 0 then c else Stdlib.compare ar1 ar2
         | Variable, Variable -> 0
         | Constant _, Variable -> ~-1
         | Variable, Constant _ -> 1