Fonctions retournant les arits des constructeurs et inductifs

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

2 files changed, 23 insertions, 1 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f8f0e45bc..59a6356ac 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -91,6 +91,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   substl (list_tabulate make_Ik ntypes) specif.(j-1)
 
 (* Arity of constructors excluding parameters and local defs *)
+
 let mis_constr_nargs indsp =
   let (mib,mip) = Global.lookup_inductive indsp in
   let recargs = dest_subterms mip.mind_recargs in
@@ -107,6 +108,20 @@ let mis_constructor_nargs_env env ((kn,i),j) =
   let mip = mib.mind_packets.(i) in 
   recarg_length mip.mind_recargs j + mib.mind_nparams
 
+let constructor_nrealargs env (ind,j) =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  recarg_length mip.mind_recargs j
+
+let constructor_nrealhyps env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_consnrealargs.(j-1) - List.length (mib.mind_params_ctxt)
+
+(* Length of arity (w/o local defs) *)
+
+let inductive_nargs env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_nrealargs + rel_context_length mib.mind_params_ctxt
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -371,4 +386,6 @@ let control_only_guard env =
   in 
   control_rec 
 
-let subst_inductive subst (kn,i) = (Mod_subst.subst_kn subst kn,i)
+let subst_inductive subst (kn,i as ind) = 
+  let kn' = Mod_subst.subst_kn subst kn in
+  if kn == kn' then ind else (kn',i)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa0306d2f..91425fe79 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -57,6 +57,11 @@ val mis_constr_nargs_env : env -> inductive -> int array
 
 val mis_constructor_nargs_env : env -> constructor -> int
 
+val constructor_nrealargs : env -> constructor -> int
+val constructor_nrealhyps : env -> constructor -> int
+
+val inductive_nargs : env -> inductive -> int
+
 type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;