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 ff8de755469b21ffb336e9f4a833e3c4016f0682..d37ec4032b6dcff26bbbcd507bcda882fd98b53a 100644 (file)
--- a/matita/components/ng_refiner/nCicUnifHint.ml
+++ b/matita/components/ng_refiner/nCicUnifHint.ml
@@ -11,6 +11,8 @@
 
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
+module Ref = NReference
+
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
@@ -19,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)
@@ -62,7 +64,10 @@ class virtual status =
    = fun o -> {< db = o#uhint_db >}
  end
 
-let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
+let dummy =
+ let uri = NUri.uri_of_string "cic:/matita/dummy/dec.con" in
+ NCic.Const (Ref.reference_of_spec uri Ref.Decl);;
+
 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
 
 let index_hint status context t1 t2 precedence =
@@ -176,11 +181,11 @@ let db () =
               in 
               let n1 = 
                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
-                 u1 (NReference.Def h1)) :: mk_rels (List.length ctx))
+                 u1 (Ref.Def h1)) :: mk_rels (List.length ctx))
               in
               let n2 = 
                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
-                 u2 (NReference.Def h2)) :: mk_rels (List.length ctx))
+                 u2 (Ref.Def h2)) :: mk_rels (List.length ctx))
               in
                 [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
               end else []
@@ -305,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
 
@@ -327,8 +332,8 @@ let look_for_hint (status:#status) metasenv subst context t1 t2 =
              end
 ;;
 
-let pp_hint t p =
-  let context, t = 
+let pp_hint _t _p =
+(*  let context, t = 
      let rec aux ctx = function
        | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
        | t -> ctx, t
@@ -344,7 +349,6 @@ let pp_hint t p =
   in
   let buff = Buffer.create 100 in
   let fmt = Format.formatter_of_buffer buff in
-(*
   F.fprintf "@[<hov>"
    F.fprintf "@[<hov>"
 (*    pp_ctx [] context *)
@@ -400,9 +404,9 @@ let generate_dot_file (status:#status) fmt =
         (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, 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;
 ;;