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

15 files changed, 39 insertions, 27 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 19c7a6cfe..4faf99a90 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -346,14 +346,14 @@ let type_case_branches env (ind,largs) (p,pj) c =
 
 
 (************************************************************************)
-(* Checking the case annotation is relevent *)
+(* Checking the case annotation is relevant *)
 
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   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)))
 
 (************************************************************************)
diff --git a/checker/term.ml b/checker/term.ml
index d9ecaaea5..35ae1121e 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -31,10 +31,10 @@ type case_printing =
   { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 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 var of each constructor *)
+    ci_pp_info     : case_printing (* not interpreted by the kernel *)
   }
 let val_ci =
   let val_cstyle = val_enum "case_style" 5 in
diff --git a/checker/term.mli b/checker/term.mli
index 1367e5813..66ba96cc5 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; }
 type case_info = {
   ci_ind : inductive;
   ci_npar : int;
-  ci_cstr_nargs : int array;
+  ci_cstr_ndecls : int array;
   ci_pp_info : case_printing;
 }
 type contents = Pos | Null
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index adf1d14e2..2fb2cb81c 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 d806c39a0..76de25344 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 685656592..d0e9d1695 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 0de831668..1ffe5eeb5 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*******************************************************************)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b20a70aa0..1eae09718 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -685,7 +685,7 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)
 				true
 				proveterminate
 				eqs
-				ci.ci_cstr_nargs.(i))
+				ci.ci_cstr_ndecls.(i))
 		    0 (Array.to_list l)) g)
 		  | _, _::_ ->
 		    (match find_call_occs  0 f_constr expr with
@@ -1321,7 +1321,7 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 	       (fun i -> mk_intros_and_continue
                           (List.rev rev_to_thin_intro) true
 			  (prove_eq termine f functional)
-			  eqs ci.ci_cstr_nargs.(i))
+			  eqs ci.ci_cstr_ndecls.(i))
 	       0 (Array.to_list l)) g)
 	   | _,_::_ ->
 	      (match find_call_occs 0 f expr with
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 7315326b7..9965e7be5 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -184,7 +184,7 @@ let sigT = Lazy.lazy_from_fun build_sigma_type
 let sigT_info = lazy
   { ci_ind       = destInd (Lazy.force sigT).typ;
     ci_npar      = 2;
-    ci_cstr_nargs = [|2|];
+    ci_cstr_ndecls = [|2|];
     ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
   }
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d46fd226e..905bb49e0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -237,7 +237,7 @@ let rec decomp_branch n nal b (avoid,env as e) c =
 
 let rec build_tree na isgoal e ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
-  let cnl = ci.ci_cstr_nargs in
+  let cnl = ci.ci_cstr_ndecls in
   List.flatten
     (list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
        (Array.length cl))
@@ -409,7 +409,7 @@ let rec detype (isgoal:bool) avoid env t =
 	  (detype_eqns isgoal avoid env ci comp)
 	  is_nondep_branch avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar,
-	   ci.ci_cstr_nargs,ci.ci_pp_info.ind_nargs)
+	   ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs)
 	  (Some p) c bl
     | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef
     | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 636f86224..3897b18e5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -145,7 +145,7 @@ let make_case_info env ind style =
   let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
-    ci_cstr_nargs = mip.mind_consnrealdecls;
+    ci_cstr_ndecls = mip.mind_consnrealdecls;
     ci_pp_info = print_info }
 
 let make_default_case_info env style ind =
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index d034bfae0..b94642c09 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -96,7 +96,7 @@ let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
 let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   match ind with
   | Some ind -> ind = ci2.ci_ind
-  | None -> cs1 = ci2.ci_cstr_nargs
+  | None -> cs1 = ci2.ci_cstr_ndecls
 
 let matches_core convert allow_partial_app pat c =
   let conv = match convert with
@@ -181,8 +181,8 @@ let matches_core convert allow_partial_app pat c =
             (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
-	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in
-	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_nargs.(1) b2' in
+	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
+	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
 	  let n = rel_context_length ctx in
           let n' = rel_context_length ctx' in
 	  if noccur_between 1 n b2 & noccur_between 1 n' b2' then
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 105672564..f9dec8f35 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -130,7 +130,7 @@ let pattern_of_constr sigma t =
     | Case (ci,p,a,br) ->
 	let cip = ci.ci_pp_info in
 	let no = Some (ci.ci_npar,cip.ind_nargs) in
-	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
+	PCase ((cip.style,ci.ci_cstr_ndecls,Some ci.ci_ind,no),
 	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b7246ad3e..95b34b8d9 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -773,7 +773,7 @@ let subterm all flags (s : strategy) : strategy =
 	    | Some (Some r) ->
 		Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
 	    | x ->
-		if array_for_all ((=) 0) ci.ci_cstr_nargs then
+		if array_for_all ((=) 0) ci.ci_cstr_ndecls then
 		  let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
 		  let found, brs' = Array.fold_left (fun (found, acc) br ->
 		    if found <> None then (found, fun x -> br :: acc x)
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 203fbbb77..8ffe4fcdb 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -54,6 +54,15 @@ Check
    | Build_B x0 x1 => f x0 x1
    end).
 
+(* Check inductive types with local definitions (constructors) *)
+
+Inductive I1 : Set := c (_:I1) (_:=0).
+
+Check (fun x:I1 =>
+  match x with
+  | c i n => (i,n)
+  end).
+
 (* Check implicit parameters of inductive types (submitted by Pierre
   Casteran and also implicit in #338) *)