+let strip_dependent_prods metasenv context t =
+ let irl = MI.identity_relocation_list_for_metavariable context in
+ let rec aux metasenv p xcontext = function
+ | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->
+ let index = MI.new_meta metasenv [] in
+ let metasenv = [index, context, t1] @ metasenv in
+ let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in
+ aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
+ | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, (S.subst (Cic.Rel 1) t2)
+ | t -> metasenv, p, None, t
+ in
+ aux metasenv 0 context t
+
+let skip_metas p =
+ let rec aux conts p =
+ if p <= 0 then conts else aux (T.id_tac :: conts) (pred p)
+ in
+ aux [] p
+
+let get_conclusion context t =
+ let rec aux p context = function
+ | Cic.Prod (name, t1, t2) ->
+ aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
+ | Cic.LetIn (name, u1, t2) ->
+ aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
+ | Cic.Cast (t2, t1) -> aux p context t2
+ | t -> p, context, t
+ in aux 0 context t
+
+let get_conclusion_dependences context t =
+ let p, context, conclusion = get_conclusion context t in
+ let rec aux l q =
+ if q <= 0 then l else
+ let b = TC.does_not_occur context (pred q) q conclusion in
+ aux (b :: l) (pred q)
+ in
+ aux [] p
+
+let solve_independents ?with_what deps =
+ let rec aux p conts = function
+ | [] -> p, conts
+ | true :: tl ->
+ let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
+ aux (succ p) (cont :: conts) tl
+ | false :: tl -> aux (succ p) conts tl
+ in
+ let p, conts = aux 0 [] deps in
+ match with_what with
+ | None -> conts
+ | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
+