Ajout mis_constructor_nargs_env

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

2 files changed, 7 insertions, 0 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 792fe6d2d..d4071bc79 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -84,6 +84,11 @@ let mis_constr_nargs_env env (kn,i) =
   let recargs = dest_subterms mip.mind_recargs in
   Array.map List.length recargs
 
+let mis_constructor_nargs_env env ((kn,i),j) =
+  let mib = Environ.lookup_mind kn env in
+  let mip = mib.mind_packets.(i) in 
+  recarg_length mip.mind_recargs j + mip.mind_nparams
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 23d0a32ca..e354f584a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -44,6 +44,8 @@ val mis_constr_nargs : inductive -> int array
 
 val mis_constr_nargs_env : env -> inductive -> int array
 
+val mis_constructor_nargs_env : env -> constructor -> int
+
 type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;