X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcoercGraph.ml;h=43e342e708f710ff27fcdb3f0aa41d00e6c4be5f;hb=0bc1d5f7eb6c9ba8603c59a4d671d4b186e48508;hp=cb33d9e324f0b41851668c37c1f237770b33342a;hpb=975ad45cc779a6bee3d450a006347cc23ca3977e;p=helm.git

diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml
index cb33d9e32..43e342e70 100644
--- a/components/cic_unification/coercGraph.ml
+++ b/components/cic_unification/coercGraph.ml
@@ -41,14 +41,15 @@ let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 let saturate_coercion ul metasenv subst context =
-  let cl = List.map CicUtil.term_of_uri ul in
+  let cl =
+   List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
   let funclass_arityl = 
-    let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+    let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
     List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
   in
   let freshmeta = CicMkImplicit.new_meta metasenv subst in
    List.map2
-    (fun arity c -> 
+    (fun arity (c,saturations) -> 
       let ty,_ =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.empty_ugraph in
@@ -57,7 +58,7 @@ let saturate_coercion ul metasenv subst context =
       let irl =
        CicMkImplicit.identity_relocation_list_for_metavariable context
       in
-       metasenv, Cic.Meta (lastmeta-1,irl),
+       metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
         match args with
            [] -> c
          | _ -> Cic.Appl (c::args)
@@ -128,18 +129,23 @@ let generate_dot_file () =
         Pp.node (CoercDb.name_of_carr carr)
           ~attrs:["href", UriManager.string_of_uri uri] fmt in
   List.iter
-    (fun (src, tgt, cl) ->
+    (fun (src, tgt, ul) ->
       let src_name = CoercDb.name_of_carr src in
       let tgt_name = CoercDb.name_of_carr tgt in
       pp_description src;
       pp_description tgt;
       List.iter
-        (fun c ->
+        (fun (u,saturations) ->
           Pp.edge src_name tgt_name
-            ~attrs:[ "label", UriManager.name_of_uri c;
-              "href", UriManager.string_of_uri c ]
+            ~attrs:[ "label",
+                     (UriManager.name_of_uri u ^
+                      if saturations = 0 then
+                       ""
+                      else
+                       "(" ^ string_of_int saturations ^ ")");
+              "href", UriManager.string_of_uri u ]
             fmt)
-        cl)
+        ul)
     l;
   Pp.trailer fmt;
   Buffer.contents buf
@@ -186,7 +192,7 @@ let coerced_arg l =
 (************************* meet calculation stuff ********************)
 let eq_uri_opt u1 u2 = 
   match u1,u2 with
-  | Some u1, Some u2 -> UriManager.eq u1 u2
+  | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
   | None,Some _ | Some _, None -> false
   | None, None -> true
 ;;