Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 24 deletions

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 71041c279..b8ea65f16 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -28,39 +28,27 @@ type inductive_error =
   | BadInduction of bool * identifier * sorts
   | NotMutualInScheme
 
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
-  decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
-   i.e. that all the types and constructors names are distinct. 
-   It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
-   types declaration. It raises an exception [InductiveError _] if there is
-   not enough abstractions in any of the terms of the field 
-   [mind_entry_inds]. *)
-
-val mind_extract_and_check_params : 
-  mutual_inductive_entry -> Sign.rel_context
+(* [mind_extract_params] extracts the parameters of an inductive
+   type declaration. *)
 
 val mind_extract_params : int -> constr -> Sign.rel_context * constr
 
-val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
+exception InductiveError of inductive_error
+
+(*s The following function does checks on inductive declarations. *)
 
-(* [mind_check_arities] checks that the types declared for all the
-   inductive types are some arities. *)
+(* [mind_check_wellformed env mie] checks that the types declared for
+   all the inductive types are arities. It checks also that
+   constructor and inductive names altogether are distinct. It raises
+   an exception [InductiveError _] if [mie] is not well-formed *)
 
-val mind_check_arities : env -> mutual_inductive_entry -> unit
+val mind_check_wellformed : env -> mutual_inductive_entry -> unit
 
 (* [cci_inductive] checks positivity and builds an inductive body *)
 
 val cci_inductive : 
-  env -> env -> path_kind -> int -> bool -> 
-   (identifier * types * identifier list * bool * bool * types array)
+  env -> env -> path_kind -> bool -> 
+   (int * identifier * types * identifier list * bool * bool * types array)
       list ->
       constraints ->
       	mutual_inductive_body