Porting to ocaml 5

[helm.git] / matita / components / ng_refiner / nDiscriminationTree.ml

diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml
index 4d746ad8baf2f74fa3ff83c4936f08d214c45891..b5338715dfd35936fc8f11f8ea9a89e6bb104c44 100644 (file)
--- 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) ;;