diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 3c1464c6c9..ad35c16c22 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> constr array -> constr array +val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array |