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 =
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
let body_metasenv = order_body_menv term body_metasenv in
debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
- debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+ debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst));
let term = rt.RT.apply_subst subst term in
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
(match rt.RT.type_of_aux' metasenv [] term ugraph with
(* 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
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 =