suppression champs inutiles dans constantes et inductifs; verification definitions inductives

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

1 files changed, 38 insertions, 10 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e57c4d295e..c60c3cf4e8 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -5,6 +5,8 @@ open Names
 open Term
 open Sign
 
+(* Inductive types (internal representation). *)
+
 type recarg = 
   | Param of int 
   | Norec 
@@ -15,11 +17,8 @@ type mutual_inductive_packet = {
   mind_consnames : identifier array;
   mind_typename : identifier;
   mind_lc : constr;
-  mind_stamp : name;
   mind_arity : typed_type;
-  mind_lamexp : constr option;
-  mind_kd : sorts list;
-  mind_kn : sorts list;
+  mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool }
 
@@ -31,12 +30,14 @@ type mutual_inductive_body = {
   mind_singl : constr option;
   mind_nparams : int }
 
-type mutual_inductive_entry = {
-  mind_entry_params : (identifier * constr) list;
-  mind_entry_inds : (identifier * constr * (identifier * constr) list) list }
-
 val mind_type_finite : mutual_inductive_body -> int -> bool
 
+
+(*s To give a more efficient access to the informations related to a given
+  inductive type, we introduce the following type [mind_specif], which
+  contains all the informations about the inductive type, including its
+  instanciation arguments. *)
+
 type mind_specif = {
   mis_sp : section_path;
   mis_mib : mutual_inductive_body;
@@ -47,9 +48,36 @@ type mind_specif = {
 val mis_ntypes : mind_specif -> int
 val mis_nconstr : mind_specif -> int
 val mis_nparams : mind_specif -> int
-val mis_kd : mind_specif -> sorts list
-val mis_kn : mind_specif -> sorts list
+val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
+
+
+(*s Declaration of inductive types. *)
+
+type mutual_inductive_entry = {
+  mind_entry_nparams : int;
+  mind_entry_finite : bool;
+  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+
+type inductive_error =
+  | NonPos of int   
+  | NotEnoughArgs of int
+  | NotConstructor  
+  | NonPar of int * int
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+exception InductiveError of inductive_error
+
+val mind_check_names : mutual_inductive_entry -> unit
+
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+val mind_extract_and_check_params : 
+  mutual_inductive_entry -> (name * constr) list
+
+val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit