- let lapply_tac status =
- let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let strip_dependent_prods metasenv context p t =
+ let rec aux metasenv add_context q = function
+ | Cic.Prod (name, t1, t2) when q > 0 ->
+ let context_for_meta = pad_context p context add_context in
+ let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in
+ let rs = MI.identity_relocation_list_for_metavariable context_for_meta in
+ let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in
+ aux metasenv (e :: add_context) (pred q) (S.subst s t2)
+ | t -> metasenv, add_context, t
+ in
+ aux metasenv [] p t
+ in
+ let mk_body bo = function
+ | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo)
+ | _ -> failwith "mk_body"
+ in
+ let lapply_tac (proof, goal) =
+ let xuri, metasenv, u, t = proof in
+(* preliminaries *)
+ let metano, context, ty = CicUtil.lookup_meta goal metasenv in