- match l with
- | [] ->
- debug_print
- (lazy
- (sprintf ":-( coercion non trovata da %s a %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- NoCoercion
- | [u] ->
- debug_print (lazy (
- sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- SomeCoercion (CicUtil.term_of_uri u)
- | u::_ ->
- debug_print (lazy (
- sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
- (List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- SomeCoercion (CicUtil.term_of_uri u)
+ (match uri with
+ None -> NoCoercion
+ | Some ul ->
+ let cl = List.map CicUtil.term_of_uri ul in
+ let arityl = List.map arity_of cl in
+ let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+ let newtl =
+ List.map2
+ (fun args c ->
+ match args with
+ | [] -> c
+ | _ -> Cic.Appl (c::args))
+ argsl cl
+ in
+ SomeCoercion newtl)