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 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
List.fold_left
(fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
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 metasenv,subst,cl =
List.fold_right
(fun (k_relev,n,te) (metasenv,subst,res) ->
let k_relev =
let metasenv,subst,cl =
List.fold_right
(fun (k_relev,n,te) (metasenv,subst,res) ->
let 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 =
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 =