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, 85 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fda1190d13..9a59a889b4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -106,91 +106,6 @@ type mutual_inductive_entry = {
   mind_entry_finite : bool;
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
-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
-
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
-
-let check_constructors_names id =
-  let rec check idset = function
-    | [] -> idset
-    | c::cl -> 
-	if Idset.mem c idset then 
-	  raise (InductiveError (SameNamesConstructors (id,c)))
-	else
-	  check (Idset.add c idset) cl
-  in
-  check
-
-(* [mind_check_names mie] checks the names of an inductive types declaration,
-   and raises the corresponding exceptions when two types or two constructors
-   have the same name. *)
-
-let mind_check_names mie =
-  let rec check indset cstset = function
-    | [] -> ()
-    | (id,_,cl,_)::inds -> 
-	if Idset.mem id indset then
-	  raise (InductiveError (SameNamesTypes id))
-	else
-	  let cstset' = check_constructors_names id cstset cl in
-	  check (Idset.add id indset) cstset' inds
-  in
-  check Idset.empty Idset.empty mie.mind_entry_inds
-
-(* [mind_extract_params mie] extracts the params from an inductive types
-   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 n c in (List.rev l,c')
-  
-let extract nparams c =
-  try mind_extract_params nparams c 
-  with UserError _ -> raise (InductiveError BadEntry)
-
-let check_params nparams params c = 
-  let eparams = fst (extract nparams c) in
-  try
-    List.iter2 
-      (fun (n1,t1) (n2,t2) ->
-	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
-	   raise (InductiveError BadEntry))
-      eparams params
-  with Invalid_argument _ ->
-    raise (InductiveError BadEntry)
-
-let mind_extract_and_check_params mie =
-  let nparams = mie.mind_entry_nparams in
-  match mie.mind_entry_inds with
-    | [] -> anomaly "empty inductive types declaration"
-    | (_,ar,_,_)::l -> 
-	let (params,_) = extract nparams ar in
-	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
-	params
-
-let mind_check_lc params mie =
-  let ntypes = List.length mie.mind_entry_inds in
-  let nparams = List.length params in
-  let check_lc (_,_,_,lc) =
-    let (lna,c) = decomp_all_DLAMV_name lc in
-    Array.iter (check_params nparams params) c;
-    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
-  in
-  List.iter check_lc mie.mind_entry_inds
-
 let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
 let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)