declarations eliminations / debuggae inductifs (debut)

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

1 files changed, 9 insertions, 3 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9dc0ca3659..433a2c1d95 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -128,7 +128,14 @@ let extract nparams c =
   with UserError _ -> raise (InductiveError BadEntry)
 
 let check_params nparams params c = 
-  if not (fst (extract nparams c) = params) then 
+  let eparams = fst (extract nparams c) in
+  try
+    List.iter2 
+      (fun (n1,t1) (n2,t2) ->
+	 if n1 <> n2 || strip_outer_cast t1 <> strip_outer_cast t2 then
+	   raise (InductiveError BadEntry))
+      eparams params
+  with Invalid_argument _ ->
     raise (InductiveError BadEntry)
 
 let mind_extract_and_check_params mie =
@@ -146,7 +153,6 @@ let mind_check_lc params mie =
   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)
+    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
   in
   List.iter check_lc mie.mind_entry_inds