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

4 files changed, 34 insertions, 9 deletions

diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index c9e135edcf..1d55a587f4 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -133,7 +133,7 @@ let compute_branches_lengths ind =
   mip.Declarations.mind_consnrealdecls
 
 let compute_inductive_nargs ind =
-  Inductiveops.inductive_nargs (Global.env()) ind
+  Inductiveops.inductive_nargs ind
 
 (* Interpreting constr as a glob_constr *)
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8963ea5ea5..3f5b3f1bf0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1654,7 +1654,7 @@ let extract_arity_signature env0 tomatchl tmsign =
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
 	  let (ind,_) = dest_ind_family indf' in
-	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs env0 ind in
+	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
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)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index f361e8b8d4..5cf84acd7a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -51,7 +51,10 @@ val mis_is_recursive :
 val mis_nf_constructor_type :
   inductive * mutual_inductive_body * one_inductive_body -> int -> constr
 
-(** Extract information from an inductive name *)
+(** {6 Extract information from an inductive name}
+
+
+Functions without env lookup in the globalenv. *)
 
 (** Arity of constructors excluding parameters and local defs *)
 val mis_constr_nargs : inductive -> int array
@@ -59,12 +62,23 @@ val mis_constr_nargs_env : env -> inductive -> int array
 
 val nconstructors : inductive -> int
 
-(** Return the lengths of parameters signature and real arguments signature *)
-val inductive_nargs : env -> inductive -> int * int
+(** @return the lengths of parameters signature and real arguments signature
+    with letin *)
+val inductive_nargs : inductive -> int * int
+val inductive_nargs_env : env -> inductive -> int * int
+
+(** @return nb of params without letin *)
+val inductive_nparams : inductive -> int
 
+(** @return param + args without letin *)
+val mis_constructor_nargs : constructor -> int
 val mis_constructor_nargs_env : env -> constructor -> int
+
+(** @return args without letin *)
 val constructor_nrealargs : env -> constructor -> int
-val constructor_nrealhyps : env -> constructor -> int
+
+(** @return args with letin *)
+val constructor_nrealhyps : constructor -> int
 
 val get_full_arity_sign : env -> inductive -> rel_context