- 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

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