X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicCoercion.ml;h=6f2443e98a45798f511279a0c5dd74e0a7e5bd07;hb=0e850ea466d664062ad1999e75c60b90aadaa084;hp=f06035604535dcd5a132f2667292f6318dc15fd2;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index f06035604..6f2443e98 100644
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -99,7 +99,7 @@ let generate_composite_closure rt c1 c2 univ arity =
     let len,names = aux [] 0 t in
     let len = len - arity in
     List.fold_left 
-      (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[]) 
+      (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) 
       names
   in
   let compose c1 nc1 c2 nc2 =
@@ -194,8 +194,8 @@ let generate_composite_closure rt c1 c2 univ arity =
   debug_print (lazy ("\nCOMPOSING"));
   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty arity in 
-  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 in
+  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
+  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
   let spline_len = saturations_for_c1 + saturations_for_c2 in
   let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
@@ -302,7 +302,7 @@ let number_if_already_defined buri name l =
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
-let close_coercion_graph rt src tgt uri =
+let close_coercion_graph rt src tgt uri baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt uri coercions in
@@ -334,9 +334,8 @@ let close_coercion_graph rt src tgt uri =
                 let name_tgt = CoercDb.name_of_carr tgt in
                 let by = List.map UriManager.name_of_uri l in
                 let name = mangle name_tgt name_src by in
-                let buri = UriManager.buri_of_uri uri in
                 let c_uri = 
-                  number_if_already_defined buri name 
+                  number_if_already_defined baseuri name 
                     (List.map (fun (_,_,u,_) -> u) acc) 
                 in
                 let named_obj =