X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnifHint.ml;h=688238983dc636149a758f333b0589129e5f215a;hb=HEAD;hp=5c7f92f999a4d10265bdd67a7d7c53375fb85b4c;hpb=3220eee6c3dd2968727c5c595d6ca78e89291b5f;p=helm.git

diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml
index 5c7f92f99..688238983 100644
--- 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)
@@ -60,7 +60,7 @@ class virtual status =
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
   method set_unifhint_status
-   : 'status. #g_status as 'status -> 'self
+   : 'status. (#g_status as 'status) -> 'self
    = fun o -> {< db = o#uhint_db >}
  end
 
@@ -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
 
@@ -403,10 +403,10 @@ let generate_dot_file (status:#status) fmt =
             edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
         (HintSet.elements dataset);
     );
-  List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
-  List.iter (fun x, y, _l, _, _ -> 
+  List.iter (fun (x, l) -> Pp.node x ~attrs:["label",l] fmt) !nodes;
+  List.iter (fun (x, y, _l, _, _) -> 
       Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
   !edges;
   edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
-  List.iter (fun _x, _y, _, p, l -> pp_hint l p) !edges;
+  List.iter (fun (_x, _y, _, p, l) -> pp_hint l p) !edges;
 ;;