X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnifHint.ml;h=688238983dc636149a758f333b0589129e5f215a;hb=8a5c30a914d7ff665218b31853c6fb4bcf58aa08;hp=d37ec4032b6dcff26bbbcd507bcda882fd98b53a;hpb=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml index d37ec4032..688238983 100644 --- a/matita/components/ng_refiner/nCicUnifHint.ml +++ b/matita/components/ng_refiner/nCicUnifHint.ml @@ -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 @@ -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; ;;