-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 apply_tac term = PT.apply_tac term in
- 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, t2
- | t -> metasenv, p, None, t
- in
- aux metasenv 0 context t
+let strip_dependent_prods metasenv context t =
+ let irl = MI.identity_relocation_list_for_metavariable context in
+ let mk_meta metasenv t =
+ let index = MI.new_meta metasenv [] in
+ let metasenv = [index, context, t] @ metasenv in
+ metasenv, Cic.Meta (index, irl)