diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 497c064172..05b0248b9e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -135,3 +135,6 @@ type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec +val lambda_implicit_lift : int -> Constr.constr -> Term.constr + +val abstract_mind_lc : int -> Int.t -> Constr.constr array -> Constr.constr array |