- 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

1 files changed, 4 insertions, 4 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 15c234b33..fbd31f24f 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;