+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
+ let lapply_tac status =
+ let proof, goal = status in
+ let _, metasenv, _subst, _, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
+ let tac =
+ if linear then
+ let hyps = get_clearables context (what :: to_what) in
+ T.then_ ~start:lapply
+ ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *)
+ else
+ lapply
+ in
+ PET.apply_tactic tac status
+ in
+ PET.mk_tactic lapply_tac
+