+ let src_carr, tgt_carr =
+ let list_remove_from_tail n l =
+ let rec aux n = function
+ | hd::tl when n > 0 -> aux (n-1) tl
+ | l when n = 0 -> l
+ | _ -> assert false
+ in
+ aux n (List.rev l)
+ in
+ let types = spline2list coer_ty in
+ match arity, list_remove_from_tail arity types with
+ | 0,tgt::src::_ ->
+ (* if ~delta is true, it is impossible to define an identity coercion *)
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ | n,_::src::_ ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.Fun arity
+ | _ -> assert false
+ in