- 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

5 files changed, 5 insertions, 9 deletions

diff --git a/configure b/configure
index de53019b72..191a9f13c1 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=7.00
+VERSION=7.0
 VERSIONSI=1.0
 DATE="November 2000"
 
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
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index c72f2ddb3c..6c76e5e888 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -55,6 +55,8 @@ let rec explain_exn_default = function
       hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >]
   | Sys.Break -> 
       hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
+  | Univ.UniverseInconsistency -> 
+      hOV 0 [< 'sTR "Error: Universe Inconsistency." >]
   | TypeError(k,ctx,te) -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >]
   | InductiveError e ->