- Correction bug calcul mind_consnrealargs, introduit à la révision

  7833, et que la révision 8644 n'avait pas corrigé dans le bon sens;
  renommage en mind_consnrealdecls pour éviter la confusion de sens
  avec mind_nrealargs
- Correction de la description du type one_inductive_body
- Ajout test avec let-in dans params et dans type constructeur 
  (fichier Case12.v)


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

7 files changed, 28 insertions, 13 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0fe01799e1..fcdd0a786e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -904,7 +904,7 @@ let rec raw_of_pat env = function
       let mib,mip = lookup_mind_specif (Global.env()) ind in
       let k = mip.Declarations.mind_nrealargs in
       let nparams = mib.Declarations.mind_nparams in
-      let cstrnargs = mip.Declarations.mind_consnrealargs in
+      let cstrnargs = mip.Declarations.mind_consnrealdecls in
       Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env)
 	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
 	avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 15c234b334..fbd31f24fc 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -118,8 +118,8 @@ type one_inductive_body = {
  (* Head normalized constructor types so that their conclusion is atomic *)
     mind_nf_lc : types array;
 
- (* Number of expected (real) arg of the constructors (no let, no params) *)
-    mind_consnrealargs : int array;
+ (* Length of the signature of the constructors (with let, w/o params) *)
+    mind_consnrealdecls : int array;
 
  (* Signature of recursive arguments in the constructors *)
     mind_recargs : wf_paths;
@@ -155,7 +155,7 @@ type mutual_inductive_body = {
   (* Number of expected parameters *)
     mind_nparams : int;
 
-  (* Number of non recursively uniform parameters *)
+  (* Number of recursively uniform (i.e. ordinary) parameters *)
     mind_nparams_rec : int;
 
   (* The context of parameters (includes let-in declaration) *)
@@ -180,7 +180,7 @@ let subst_const_body sub cb = {
 
 let subst_mind_packet sub mbp = 
   { mind_consnames = mbp.mind_consnames;
-    mind_consnrealargs = mbp.mind_consnrealargs;
+    mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_typename = mbp.mind_typename;
     mind_nf_lc = 
       array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 10559ffe15..bd689ced37 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -105,8 +105,8 @@ type one_inductive_body = {
  (* Head normalized constructor types so that their conclusion is atomic *)
     mind_nf_lc : types array;
 
- (* Number of expected (real) arg of the constructors (no let, no params) *)
-    mind_consnrealargs : int array;
+ (* Length of the signature of the constructors (with let, w/o params) *)
+    mind_consnrealdecls : int array;
 
  (* Signature of recursive arguments in the constructors *)
     mind_recargs : wf_paths;
@@ -142,7 +142,7 @@ type mutual_inductive_body = {
   (* Number of expected parameters *)
     mind_nparams : int;
 
-  (* Number of non recursively uniform parameters *)
+  (* Number of recursively uniform (i.e. ordinary) parameters *)
     mind_nparams_rec : int;
 
   (* The context of parameters (includes let-in declaration) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2398375699..103a5982ef 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -543,7 +543,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let nf_lc = if nf_lc = lc then lc else nf_lc in
     let consnrealargs =
-      Array.map (fun (d,b) -> rel_context_nhyps d - nparamargs) splayed_lc in
+      Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+	splayed_lc in
     (* Elimination sorts *)
     let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
     let kelim = allowed_sorts env issmall isunit ar_sort in
@@ -568,7 +569,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_consnames = Array.of_list cnames;
-      mind_consnrealargs = consnrealargs;
+      mind_consnrealdecls = consnrealargs;
       mind_user_lc = lc;
       mind_nf_lc = nf_lc;
       mind_recargs = recarg;    
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 92b919c7eb..3adbd6e36a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -278,7 +278,7 @@ let check_case_info env indsp ci =
   if
     (indsp <> ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
-    (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
+    (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3e43eee4dd..c0902526ac 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -114,7 +114,7 @@ let constructor_nrealargs env (ind,j) =
 
 let constructor_nrealhyps env (ind,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_consnrealargs.(j-1) - rel_context_length (mib.mind_params_ctxt)
+  mip.mind_consnrealdecls.(j-1)
 
 (* Length of arity (w/o local defs) *)
 
@@ -131,7 +131,7 @@ let make_case_info env ind style pats_source =
       source    = pats_source } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
-    ci_cstr_nargs = mip.mind_consnrealargs;
+    ci_cstr_nargs = mip.mind_consnrealdecls;
     ci_pp_info = print_info }
 
 let make_default_case_info env style ind =
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 20073aa73b..f6a0d57801 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -57,3 +57,17 @@ Check
      | nil'' => 0
      | cons'' n l0 => S (length (mult2 n) l0)
      end).
+
+(* Check let-in in both parameters and in constructors *)
+
+Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
+  | nil''' : list''' A a (a,a)
+  | cons''' : 
+     forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a).
+
+Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) 
+  {struct l} : nat :=
+  match l with
+  | nil''' => 0
+  | cons''' _ m l0 => S (length''' A a m l0)
+  end.