Inductiveops.nb_*{,_env} cleaning

- Functions without _env use the global env.
- More comments about when letin are counted.

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

1 files changed, 14 insertions, 3 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 15fd226f1a..f0e643f5ab 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -106,6 +106,10 @@ 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 (indsp,j) =
+  let (mib,mip) = Global.lookup_inductive indsp in
+  recarg_length mip.mind_recargs j + mib.mind_nparams
+
 let mis_constructor_nargs_env env ((kn,i),j) =
   let mib = Environ.lookup_mind kn env in
   let mip = mib.mind_packets.(i) in
@@ -115,8 +119,8 @@ 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
+let constructor_nrealhyps (ind,j) =
+  let (mib,mip) = Global.lookup_inductive ind in
   mip.mind_consnrealdecls.(j-1)
 
 let get_full_arity_sign env ind =
@@ -129,7 +133,14 @@ let nconstructors ind =
 
 (* Length of arity (w/o local defs) *)
 
-let inductive_nargs env ind =
+let inductive_nparams ind =
+  (fst (Global.lookup_inductive ind)).mind_nparams
+
+let inductive_nargs ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
+
+let inductive_nargs_env env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)