- 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:(
- skip_metas p @ solve_independents ?with_what deps
- )
- )
+ let rec aux metasenv metas conts tw = function
+ | Some hm, _ when hm <= 0 -> metasenv, metas, conts
+ | xhm, Cic.Prod (Cic.Name _, t1, t2) ->
+ let metasenv, meta, index = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) (conts @ [id_tac, index]) tw (xhm, (S.subst meta t2))
+ | xhm, Cic.Prod (Cic.Anonymous, t1, t2) ->
+ let xhm, pos, tac, tw = update_counters (xhm, tw) in
+ let metasenv, meta, index = mk_meta metasenv t1 in
+ let conts = if pos then (tac, index) :: conts else conts @ [tac, index] in
+ aux metasenv (meta :: metas) conts tw (xhm, (S.subst meta t2))
+ | _, t -> metasenv, metas, conts