fixed confusion between number of cstr arguments and number of pattern variables (which include let-ins in cstr type)

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

4 files changed, 12 insertions, 9 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index adf1d14e23..2fb2cb81ce 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -125,7 +125,7 @@ type one_inductive_body = {
     mind_nf_lc : types array;
 
  (* Length of the signature of the constructors (with let, w/o params)
-    (not used in the kernel) *)
+    (not to be used in the kernel!) *)
     mind_consnrealdecls : int array;
 
  (* Signature of recursive arguments in the constructors *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d806c39a09..76de25344e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -367,7 +367,7 @@ let check_case_info env indsp ci =
   if
     not (eq_ind indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
-    (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
+    (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
@@ -521,7 +521,10 @@ let lookup_subterms env ind =
    Rq: if branch is not eta-long, then the recursive information
    is not propagated to the missing abstractions *)
 let case_branches_specif renv c_spec ci lbr =
-  let ind = ci.ci_ind in
+  let car =
+    let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
+    let v = dest_subterms mip.mind_recargs in
+    Array.map List.length v in
   let rec push_branch_args renv lrec c =
     match lrec with
         ra::lr ->
@@ -545,7 +548,7 @@ let case_branches_specif renv c_spec ci lbr =
 	      | Dead_code -> Array.create nca (lazy Dead_code)
 	      | Not_subterm -> Array.create nca (lazy Not_subterm)) in
 	 list_tabulate (fun j -> (Lazy.force cs).(j)) nca)
-      ci.ci_cstr_nargs in
+      car in
   assert (Array.length sub_spec = Array.length lbr);
   array_map2 (push_branch_args renv) sub_spec lbr
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 685656592f..d0e9d16950 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -31,7 +31,7 @@ type case_printing =
 type case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_nargs : int array; (* number of real args of each constructor *)
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
     ci_pp_info    : case_printing (* not interpreted by the kernel *)
   }
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 0de8316689..1ffe5eeb5f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -46,10 +46,10 @@ type case_printing =
     style     : case_style }
 (* the integer is the number of real args, needed for reduction *)
 type case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_nargs : int array; (* number of real args of each constructor *)
-    ci_pp_info    : case_printing (* not interpreted by the kernel *)
+  { ci_ind         : inductive;
+    ci_npar        : int;
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
+    ci_pp_info     : case_printing (* not interpreted by the kernel *)
   }
 
 (*s*******************************************************************)