- HExtlib.list_mapi (fun bo fno ->
- (* potrebbe anche aggiungere un arg di cui fa push alle safe *)
- eat_or_subst_lambdas ~subst ~metasenv (fno=i) j bo fa args k) bos
+ HExtlib.list_mapi
+ (fun bo fno ->
+ let bo_and_k =
+ eat_or_subst_lambdas ~subst ~metasenv j bo fa args new_k
+ in
+ if
+ fno = i &&
+ List.length args > recno &&
+ (*case where the recursive argument is already really_smaller *)
+ is_really_smaller r_uri r_len ~subst ~metasenv k
+ (List.nth args recno)
+ then
+ let bo,(context, _, _ as new_k) = bo_and_k in
+ let bo, context' =
+ eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in
+ let new_context_part,_ =
+ HExtlib.split_nth (List.length context' - List.length context)
+ context' in
+ let k = List.fold_right shift_k new_context_part new_k in
+ let context, recfuns, x = k in
+ let k = context, (1,Safe)::recfuns, x in
+ bo,k
+ else
+ bo_and_k
+ ) bos