From d608222a594861efbae01e71018b8dcfc143e09a Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 15 Dec 2000 14:26:58 +0000 Subject: - suppression mind_extract_params - contraintes univers parametres inductifs prises en compte - exception UniverseInconsistency donne un message "Error: Universe Inconsistency" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/indtypes.ml | 3 +-- kernel/indtypes.mli | 5 ----- kernel/safe_typing.ml | 2 +- 3 files changed, 2 insertions(+), 8 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3