- let rec pad_context p context add_context =
- if List.length add_context >= p then add_context @ context
- else pad_context p context (None :: add_context)
- 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"