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, 18 insertions, 4 deletions

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index f361e8b8d..5cf84acd7 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