+ let src_carr, tgt_carr, no_args =
+ let get_classes arity saturations l =
+ (* this is the ackerman's function revisited *)
+ let rec aux = function
+ 0,0,None,tgt::src::_ -> src,Some (`Class tgt)
+ | 0,0,target,src::_ -> src,target
+ | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
+ | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
+ | arity,saturations,None,_::tl ->
+ aux (arity, saturations, Some `Funclass, tl)
+ | arity,saturations,target,_::tl ->
+ aux (arity - 1, saturations, target, tl)
+ | _ -> assert false
+ in
+ aux (arity,saturations,None,List.rev l)
+ in
+ let types = spine2list coer_ty in
+ let src,tgt = get_classes arity saturations types in
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
+ (match tgt with
+ | None -> assert false
+ | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+ List.length types - 1
+ in
+ let already_in_obj src_carr tgt_carr uri obj =