+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
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?to_what what =
+ let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
+ let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
+ let solve_conclusion_tac ?with_what p deps =
+ T.then_ ~start:(intros_tac ())
+ ~continuation:(
+ T.thens ~start:(PT.apply_tac what)
+ ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ]
+(* skip_metas p @ solve_independents ?with_what deps *)
+ )
+ )
+ in
+ let lapply_tac (proof, goal) =
+ let xuri, metasenv, u, t = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+ let lemma = FNG.clean_dummy_dependent_types lemma in
+ match strip_dependent_prods metasenv context lemma with
+ | metasenv, p, Some premise, conclusion ->
+ let deps = get_conclusion_dependences context conclusion in
+ let inner_tac = match to_what with
+ | None ->
+ T.thens ~start:(cut_tac premise)
+ ~continuations:[
+ solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
+ T.id_tac
+ ]
+ | Some with_what ->
+ solve_conclusion_tac ~with_what p deps
+ in
+ let outer_tac =
+ T.thens ~start:(cut_tac conclusion)
+ ~continuations:[T.id_tac; T.id_tac (* inner_tac *)]
+ in
+*)