diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
3 files changed, 2 insertions, 8 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f10e59c9c7..2307a405f5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -74,8 +74,7 @@ let mind_check_names mie = declaration, and checks that they are all present (and all the same) for all the given types. *) -let mind_extract_params n c = - let (l,c') = decompose_prod_n_assum n c in (l,c') +let mind_extract_params = decompose_prod_n_assum let mind_check_arities env mie = let check_arity id c = diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index b8ea65f16e..be97f52494 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -28,11 +28,6 @@ type inductive_error = | BadInduction of bool * identifier * sorts | NotMutualInScheme -(* [mind_extract_params] extracts the parameters of an inductive - type declaration. *) - -val mind_extract_params : int -> constr -> Sign.rel_context * constr - exception InductiveError of inductive_error (*s The following function does checks on inductive declarations. *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a6934b9dc0..925ca9bf0f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -470,7 +470,7 @@ let add_mind sp mie env = (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds params_arity_list - ([],Constraint.empty) in + ([],cst) in (* Finally, we build the inductive packet and push it to env *) let kind = kind_of_path sp in |