Abstraction du type typed_type (un pas vers les jugements 2 niveaux)

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

1 files changed, 39 insertions, 0 deletions

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 1e675b2c0..e955f6009 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,11 +9,50 @@ open Inductive
 open Environ
 (*i*)
 
+
+(*s The different kinds of errors that may result of a malformed inductive
+  definition. *)
+
+type inductive_error =
+  | NonPos of name list * constr * constr
+  | NotEnoughArgs of name list * constr * constr
+  | NotConstructor of name list * constr * constr
+  | NonPar of name list * constr * int * constr * constr
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+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 -> (name * constr) list
+
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+
+val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
 
 val mind_check_arities : env -> mutual_inductive_entry -> unit
 
+(* [cci_inductive] checks positivity and builds an inductive body *)
+
 val cci_inductive : 
   env -> env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->