Remplacement du tableau du nombre d'args utiles pour la réduction des Cases par le nombre d'args inutiles + vérification dans le noyau

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

1 files changed, 6 insertions, 3 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3eef05bf0..10d0bb611 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -369,13 +369,16 @@ let check_branches_message env sigma cj (explft,lft) =
   done;
   !univ)
 
-let judge_of_case env sigma ci pj cj lfj =
+let nparams_of (IndType (IndFamily (mis,_),_)) = mis_nparams mis 
+
+let judge_of_case env sigma (np,_ as ci) pj cj lfj =
   let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in
   let indspec =
     try find_rectype env sigma (body_of_type cj.uj_type)
     with Induc -> error_case_not_inductive CCI env cj in
-  let (bty,rslty,univ) =
-    type_case_branches env sigma indspec pj cj.uj_val in
+  if np <> nparams_of indspec then 
+    anomaly "judge_of_case: wrong parameters number";
+  let (bty,rslty,univ) = type_case_branches env sigma indspec pj cj.uj_val in
   let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in
   let univ' = check_branches_message env sigma cj (bty,lft) in
   ({ uj_val  = mkMutCase (ci, (nf_betaiota pj.uj_val), cj.uj_val, Array.map j_val lfj);