X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=b5338715dfd35936fc8f11f8ea9a89e6bb104c44;hb=e082eec771e24842f29a01fa258f7c80bc2db599;hp=4d746ad8baf2f74fa3ff83c4936f08d214c45891;hpb=2815c74c03f38089d0e27aba00e2280223b0f76f;p=helm.git

diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml
index 4d746ad8b..b5338715d 100644
--- a/matita/components/ng_refiner/nDiscriminationTree.ml
+++ b/matita/components/ng_refiner/nDiscriminationTree.ml
@@ -29,7 +29,7 @@ open Discrimination_tree
 
 module TermOT : Set.OrderedType with type t = NCic.term = struct 
   type t = NCic.term 
-  let compare = Pervasives.compare 
+  let compare = Stdlib.compare 
 end
 
 module TermSet = Set.Make(TermOT)
@@ -37,7 +37,7 @@ module TermSet = Set.Make(TermOT)
 module TermListOT : Set.OrderedType with type t = NCic.term list =
  struct
    type t = NCic.term list
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module TermListSet : Set.S with type elt = NCic.term list =
@@ -91,8 +91,8 @@ let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NReference.compare u1 u2 in
-       if x = 0 then Pervasives.compare a1 a2 else x
-  | e1,e2 -> Pervasives.compare e1 e2
+       if x = 0 then Stdlib.compare a1 a2 else x
+  | e1,e2 -> Stdlib.compare e1 e2
 ;;
 
 let string_of_path l = String.concat "." (List.map ppelem l) ;;