+let infer_dependent ~headless context metasenv = function
+ | [] -> assert false
+ | [t] -> [false, t]
+ | he::tl as l ->
+ if headless then
+ List.map (function s -> false,s) l
+ else
+ try
+ let hety,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv context (Deannotate.deannotate_term he)
+ CicUniv.oblivion_ugraph
+ in
+ let fstorder t =
+ match CicReduction.whd context t with
+ | Cic.Prod _ -> false
+ | _ -> true
+ in
+ let rec dummify_last_tgt t =
+ match CicReduction.whd context t with
+ | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt)
+ | _ -> Cic.Implicit None
+ in
+ let rec aux ty = function
+ | [] -> []
+ | t::tl ->
+ match
+ FreshNamesGenerator.clean_dummy_dependent_types
+ (dummify_last_tgt ty)
+ with
+ | Cic.Prod (n,src,tgt) ->
+ (n <> Cic.Anonymous && fstorder src, t) ::
+ aux (CicSubstitution.subst
+ (Deannotate.deannotate_term t) tgt) tl
+ | _ -> assert false
+ in
+ (false, he) :: aux hety tl
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+;;
+
+let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =