Porting to ocaml 5

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

diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml
index 5c7f92f999a4d10265bdd67a7d7c53375fb85b4c..d37ec4032b6dcff26bbbcd507bcda882fd98b53a 100644 (file)
--- a/matita/components/ng_refiner/nCicUnifHint.ml
+++ b/matita/components/ng_refiner/nCicUnifHint.ml
@@ -21,14 +21,14 @@ with type t = int * NCic.term  * NCic.term * NCic.term =
   struct
         (* precedence, skel1, skel2, term *)
         type t = int * NCic.term * NCic.term * NCic.term
-        let compare = Pervasives.compare
+        let compare = Stdlib.compare
   end
 
 module EOT : Set.OrderedType 
 with type t = int * NCic.term =
   struct
         type t = int * NCic.term 
-        let compare = Pervasives.compare
+        let compare = Stdlib.compare
   end
 
 module HintSet = Set.Make(HOT)
@@ -310,7 +310,7 @@ let look_for_hint (status:#status) metasenv subst context t1 t2 =
     rc
   in
   let rc = 
-    List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
+    List.sort (fun (x,_,_,_) (y,_,_,_) -> Stdlib.compare x y) rc
   in 
   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in