let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
- let parameters, arguments = HExtlib.split_nth leftno args in
+ let parameters, arguments = HExtlib.split_nth "NR 1" leftno args in
let outtype =
match outtype with
| C.Implicit _ as ot ->
List.fold_left
(fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
- let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
+ let sx_context_ty_rev,_= HExtlib.split_nth "NR 2" leftno (List.rev context) in
let metasenv,subst,cl =
List.fold_right
(fun (k_relev,n,te) (metasenv,subst,res) ->
let k_relev =
- try snd (HExtlib.split_nth leftno k_relev)
+ try snd (HExtlib.split_nth "NR 3" leftno k_relev)
with Failure _ -> k_relev in
let te = NCicTypeChecker.debruijn uri len [] te in
let metasenv, subst, te, _ = check_type metasenv subst tys te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =
- HExtlib.split_nth (List.length tys) (List.rev context) in
+ HExtlib.split_nth "NR 4" (List.length tys) (List.rev context) in
let sx_context_te_rev,_ =
- HExtlib.split_nth leftno chopped_context_rev in
+ HExtlib.split_nth "NR 5" leftno chopped_context_rev in
let metasenv,subst,_ =
try
List.fold_left2