+ let update_counters = function
+ | None, [] -> None, T.id_tac, []
+ | None, to_what :: tail -> None, PT.apply_tac ~term:to_what, tail
+ | Some hm, [] -> Some (pred hm), T.id_tac, []
+ | Some hm, to_what :: tail -> Some (pred hm), PT.apply_tac ~term:to_what, tail
+ in
+ 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) ((T.id_tac, index) :: conts) tw (xhm, (S.subst meta t2))
+ | xhm, Cic.Prod (Cic.Anonymous, t1, t2) ->
+ let xhm, tac, tw = update_counters (xhm, tw) in
+ let metasenv, meta, index = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) ((tac, index) :: conts) tw (xhm, (S.subst meta t2))
+ | _, t -> metasenv, metas, conts