+ let rec aux metasenv metas = function
+ | Cic.Prod (Cic.Name _ as name, t1, t2) ->
+ let metasenv, meta = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) (S.subst meta t2)
+ | Cic.Prod (Cic.Anonymous, t1, _) ->
+ let metasenv, meta = mk_meta metasenv t1 in
+ metasenv, metas, Some meta
+ | t -> metasenv, metas, None
+ in
+ aux metasenv [] t
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?to_what what =
+ let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term 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, metas, Some meta ->
+ let pippo = Cic.Appl (what :: List.rev (meta :: metas)) in
+ Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr;
+ let outer_tac = letin_tac pippo in
+ let status = (xuri, metasenv, u, t), goal in
+ PET.apply_tactic outer_tac status
+ | metasenv, metas, None ->
+ failwith "lapply_tac: not implemented"
+ in
+ PET.mk_tactic lapply_tac
+
+(*
+
+