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, 0 insertions, 36 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c9857daaf8..c5520cf493 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -112,42 +112,6 @@ type mutual_inductive_entry = {
   mind_entry_finite : bool;
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
-(*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
-
 val inductive_of_constructor : constructor -> inductive
 
 val ith_constructor_of_inductive : inductive -> int -> constructor