From 141738906969de8cb9503823bc1866b0c83fc17e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 18 Nov 2003 10:50:35 +0000
Subject: Ajout mis_constructor_nargs_env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4936 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml  | 5 +++++
 pretyping/inductiveops.mli | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 792fe6d2d9..d4071bc792 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 23d0a32ca5..e354f584a7 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;
-- 
cgit v1.2.3