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

3 files changed, 7 insertions, 7 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