A tentative uniform naming policy in module Inductiveops.

- realargs: refers either to the indices of an inductive, or to the proper args
  of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs

- realdecls: refers to the defining context of indices or proper args
  of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls

29 files changed, 228 insertions, 133 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 484d64973..cd6d0afee 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -254,7 +254,7 @@ type one_inductive_body = {
 
     mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
 
-    mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *)
+    mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
     mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index c705a707f..d38df793f 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -557,7 +557,7 @@ let subst_mind_packet sub mbp =
     mind_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
-    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
+    mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
     mind_nb_constant = mbp.mind_nb_constant;
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 14710c10b..49d78a7a6 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -160,7 +160,7 @@ let typecheck_arity env params inds =
         if ind.mind_nrealargs <> nrealargs then
              failwith "bad number of real inductive arguments";
 	let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in
-        if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then
+        if ind.mind_nrealdecls <> nrealargs_ctxt then
              failwith "bad length of real inductive arguments signature";
 	(* We do not need to generate the universe of full_arity; if
 	   later, after the validation of the inductive definition,
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 9d739b04c..f6cc5c565 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -59,7 +59,7 @@ let make_inductive_subst mib u =
     Univ.make_universe_subst u mib.mind_universes
   else Univ.empty_level_subst
 
-let inductive_params_ctxt (mib,u) = 
+let inductive_paramdecls (mib,u) = 
   let subst = make_inductive_subst mib u in
     subst_univs_level_context subst mib.mind_params_ctxt
 
@@ -361,10 +361,10 @@ let extended_rel_list n hyps =
   reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (Ind ind,
-       List.map (lift mip.mind_nrealargs_ctxt) params
+       List.map (lift mip.mind_nrealdecls) params
        @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index a919b86c2..036bf1d5e 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -85,6 +85,8 @@
   renamed into replace_term_occ_modulo and
   replace_term_occ_decl_modulo).
 
+- API of Inductiveops made more uniform (see commit log or file itself).
+
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5ce7f8f91..9c2f8bcd3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -165,7 +165,7 @@ let in_debugger = ref false
 
 let add_patt_for_params ind l =
   if !in_debugger then l else
-    Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -275,7 +275,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
      not explicit application. *)
   match pat with
     | PatCstr(loc,cstrsp,args,na)
-	when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp ->
+	when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 195bd31fe..95d902fd4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -876,12 +876,11 @@ let check_or_pat_variables loc ids idsl =
 (** Use only when params were NOT asked to the user.
     @return if letin are included *)
 let check_constructor_length env loc cstr len_pl pl0 =
-  let nargs = Inductiveops.mis_constructor_nargs cstr in
   let n = len_pl + List.length pl0 in
-  if Int.equal n nargs then false else
-    (Int.equal n ((fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr)) ||
+  if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
+    (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
       (error_wrong_numarg_constructor_loc loc env cstr
-        (nargs - (Inductiveops.inductive_nparams (fst cstr))))
+         (Inductiveops.constructor_nrealargs cstr)))
 
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
   let impl_list = if Int.equal len_pl1 0
@@ -902,26 +901,23 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
   in aux 0 (impl_list,pl2)
 
 let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
-  let nargs = Inductiveops.mis_constructor_nargs c in
-  let nargs' = (fst (Inductiveops.inductive_nargs (fst c)))
-    + Inductiveops.constructor_nrealhyps c in
+  let nargs = Inductiveops.constructor_nallargs c in
+  let nargs' = Inductiveops.constructor_nalldecls c in
   let impls_st = implicits_of_global (ConstructRef c) in
   add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
-  let (mib,mip) = Global.lookup_inductive c in
-  let nparams = mib.Declarations.mind_nparams in
-  let nargs = mip.Declarations.mind_nrealargs + nparams in
-  let nparams', nrealargs' = inductive_nargs_env env c in
+  let nallargs = inductive_nallargs_env env c in
+  let nalldecls = inductive_nalldecls_env env c in
   let impls_st = implicits_of_global (IndRef c) in
   add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c)
-    nargs (nrealargs' + nparams') impls_st len_pl1 pl2
+    nallargs nalldecls impls_st len_pl1 pl2
 
 (** Do not raise NotEnoughArguments thanks to preconditions*)
 let chop_params_pattern loc ind args with_letin =
   let nparams = if with_letin
-    then fst (Inductiveops.inductive_nargs ind)
+    then Inductiveops.inductive_nparamdecls ind
     else Inductiveops.inductive_nparams ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
@@ -942,8 +938,8 @@ let find_constructor loc add_params ref =
   cstr, (function (ind,_ as c) -> match add_params with
     |Some nb_args ->
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealhyps c)
-          then fst (Inductiveops.inductive_nargs ind)
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls c)
+          then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
       List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 85dac4bfc..f76f401b4 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -123,18 +123,18 @@ type one_inductive_body = {
 
     mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
 
-    mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *)
+    mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
     mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
     mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
 
-    mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
+    mind_consnrealargs : int array;
+ (** Number of expected proper arguments of the constructors (w/o params)
     (not used in the kernel) *)
 
-    mind_consnrealargs : int array;
- (** Length of the signature of the constructors (w/o let, w/o params)
+    mind_consnrealdecls : int array;
+ (** Length of the signature of the constructors (with let, w/o params)
     (not used in the kernel) *)
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9d2382f6e..4524b55bb 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -216,7 +216,7 @@ let subst_mind_packet sub mbp =
     mind_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
-    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
+    mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
     mind_nb_constant = mbp.mind_nb_constant;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9c83ba1a9..89d2d7b67 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -728,7 +728,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_arity = arkind;
 	mind_arity_ctxt = ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
+	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealdecls;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f08843a17..163bc3a42 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -55,7 +55,7 @@ let make_inductive_subst mib u =
     make_universe_subst u mib.mind_universes
   else Univ.empty_level_subst
 
-let inductive_params_ctxt (mib,u) = 
+let inductive_paramdecls (mib,u) = 
   let subst = make_inductive_subst mib u in
     Vars.subst_univs_level_context subst mib.mind_params_ctxt
 
@@ -347,10 +347,10 @@ let extended_rel_list n hyps =
   reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       List.map (lift mip.mind_nrealargs_ctxt) params
+       List.map (lift mip.mind_nrealdecls) params
        @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
@@ -427,7 +427,7 @@ let type_case_branches env (pind,largs) pj c =
   let p = pj.uj_val in
   let () = is_correct_arity env c pj pind specif params in
   let lc = build_branches_type pind specif params p in
-  let ty = build_case_type env (snd specif).mind_nrealargs_ctxt p c realargs in
+  let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in
   (lc, ty)
 
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 05b0248b9..8bd1a5605 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -39,7 +39,7 @@ val make_inductive_subst : mutual_inductive_body -> universe_instance -> univers
 
 val inductive_instance : mutual_inductive_body -> universe_instance
 val inductive_context : mutual_inductive_body -> universe_context
-val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context
+val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
 
 val instantiate_inductive_constraints : 
   mutual_inductive_body -> universe_level_subst -> constraints
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 99cfa7083..621aab8a0 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -146,8 +146,8 @@ let compute_branches_lengths ind =
   let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
   mip.Declarations.mind_consnrealdecls
 
-let compute_inductive_nargs ind =
-  Inductiveops.inductive_nargs ind
+let compute_inductive_ndecls ind =
+  snd (Inductiveops.inductive_ndecls ind)
 
 (* Interpreting constr as a glob_constr *)
 
@@ -188,7 +188,7 @@ let rec interp_xml_constr = function
       let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
       in
       let mat = simple_cases_matrix_of_branches ind brs in
-      let nparams,n = compute_inductive_nargs ind in
+      let n = compute_inductive_ndecls ind in
       let nal,rtn = return_type_of_predicate ind n p in
       GCases (loc,RegularStyle,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 73c050bb2..70aaa0c0f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -65,7 +65,7 @@ let rec decompose_term env sigma t=
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
-	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
+	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
 	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cce6aff28..618717cde 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -793,7 +793,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
 and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs_env env ip in
+  let ni = constructors_nrealargs_env env ip in
   let br_size = Array.length br in
   assert (Int.equal (Array.length ni) br_size);
   if Int.equal br_size 0 then begin
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 41970fce8..40abdb68b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -304,7 +304,7 @@ let build_constructors_of_type ind' argl =
 		  Impargs.implicits_of_global constructref
 		in
 		let cst_narg =
-		  Inductiveops.mis_constructor_nargs_env
+		  Inductiveops.constructor_nallargs_env
 		    (Global.env ())
 		    construct
 		in
@@ -388,7 +388,7 @@ let rec pattern_to_term_and_type env typ  = function
 	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
+	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
 	  constr
       in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5efaf7954..4cdea414e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -427,7 +427,7 @@ let rec pattern_to_term  = function
 	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
+	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
 	  constr
       in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3f1bead36..737c9fa1b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -265,7 +265,7 @@ let rec find_row_ind = function
 
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
-  let arsign = get_full_arity_sign env indu in
+  let arsign = inductive_alldecls_env env indu in
   let hole_source = match tmloc with
     | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
     | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in
@@ -1636,7 +1636,7 @@ let build_inversion_problem loc env sigma tms t =
     | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
     | App (f,v) when isConstruct f ->
 	let cstr,u = destConstruct f in
-	let n = constructor_nrealargs env cstr in
+	let n = constructor_nrealargs_env env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_map' reveal_pattern l acc in
 	PatCstr (Loc.ghost,cstr,l,Anonymous), acc
@@ -1764,7 +1764,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
 	  let ((ind,u),_) = dest_ind_family indf' in
-	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs_env env0 ind in
+	  let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7793216d5..f754f9f3f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -300,7 +300,7 @@ let get_coercion_constructor coe =
   in
   match kind_of_term c with
   | Construct (cstr,u) ->
-      (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
+      (cstr, Inductiveops.constructor_nrealargs cstr -1)
   | _ ->
       raise Not_found
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 92a29fce7..8bff91602 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -36,7 +36,7 @@ let print_universes = Flags.univ_print
 
 let encode_inductive r =
   let indsp = global_inductive r in
-  let constr_lengths = mis_constr_nargs indsp in
+  let constr_lengths = constructors_nrealargs indsp in
   (indsp,constr_lengths)
 
 (* Parameterization of the translation from constr to ast      *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index dba151014..a12fe6b67 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -70,7 +70,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	(RecursionSchemeError
 	   (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
   in
-  let ndepar = mip.mind_nrealargs_ctxt + 1 in
+  let ndepar = mip.mind_nrealdecls + 1 in
 
   (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 313bf6110..ed243bebe 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -104,86 +104,159 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   let univsubst = make_inductive_subst mib u in
     substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1))
 
-(* Arity of constructors excluding parameters and local defs *)
+(* Number of constructors *)
 
-let mis_constr_nargs indsp =
-  let (mib,mip) = Global.lookup_inductive indsp in
-  let recargs = dest_subterms mip.mind_recargs in
-  Array.map List.length recargs
+let nconstructors ind =
+  let (_,mip) = Global.lookup_inductive ind in
+  Array.length mip.mind_consnames
 
-let mis_constr_nargs_env env (kn,i) =
-  let mib = Environ.lookup_mind kn env in
-  let mip = mib.mind_packets.(i) in
-  let recargs = dest_subterms mip.mind_recargs in
-  Array.map List.length recargs
+let nconstructors_env env ind =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  Array.length mip.mind_consnames
 
-(* Arity of constructors excluding local defs *)
+(* Arity of constructors excluding parameters, excluding local defs *)
 
-let mis_constructor_nargs (indsp,j) =
+let constructors_nrealargs ind =
+  let (_,mip) = Global.lookup_inductive ind in
+  mip.mind_consnrealargs
+
+let constructors_nrealargs_env env ind =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_consnrealargs
+
+(* Arity of constructors excluding parameters, including local defs *)
+
+let constructors_nrealdecls ind =
+  let (_,mip) = Global.lookup_inductive ind in
+  mip.mind_consnrealdecls
+
+let constructors_nrealdecls_env env ind =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_consnrealdecls
+
+(* Arity of constructors including parameters, excluding local defs *)
+
+let constructor_nallargs (indsp,j) =
   let (mib,mip) = Global.lookup_inductive indsp in
-  recarg_length mip.mind_recargs j + mib.mind_nparams
+  mip.mind_consnrealargs.(j-1) + mib.mind_nparams
 
-let mis_constructor_nargs_env env ((kn,i),j) =
+let constructor_nallargs_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 + mib.mind_nparams
+  mip.mind_consnrealargs.(j-1) + mib.mind_nparams
 
-(* Arity of constructors with arg and defs *)
+(* Arity of constructors including params, including local defs *)
 
-let mis_constructor_nhyps (indsp,j) =
+let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *)
   let (mib,mip) = Global.lookup_inductive indsp in
-   mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+  mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
 
-let mis_constructor_nhyps_env env ((kn,i),j) =
+let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *)
   let mib = Environ.lookup_mind kn env in
   let mip = mib.mind_packets.(i) in
-   mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+  mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+
+(* Arity of constructors excluding params, excluding local defs *)
+
+let constructor_nrealargs (ind,j) =
+  let (_,mip) = Global.lookup_inductive ind in
+  mip.mind_consnrealargs.(j-1)
 
-let constructor_nrealargs env (ind,j) =
+let constructor_nrealargs_env env (ind,j) =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
-  recarg_length mip.mind_recargs j
+  mip.mind_consnrealargs.(j-1)
 
-let constructor_nrealhyps (ind,j) =
-  let (mib,mip) = Global.lookup_inductive ind in
+(* Arity of constructors excluding params, including local defs *)
+
+let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *)
+  let (_,mip) = Global.lookup_inductive ind in
   mip.mind_consnrealdecls.(j-1)
 
-let get_full_arity_sign env (ind,u) =
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let subst = Inductive.make_inductive_subst mib u in
-    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
+let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *)
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_consnrealdecls.(j-1)
 
-let nconstructors ind =
-  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
-  Array.length mip.mind_consnames
+(* Length of arity, excluding params, including local defs *)
 
-let mis_constructor_has_local_defs (indsp,j) =
-  let (mib,mip) = Global.lookup_inductive indsp in
-  let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
-  let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
-  not (Int.equal l1 l2)
+let inductive_nrealdecls ind =
+  let (_,mip) = Global.lookup_inductive ind in
+  mip.mind_nrealdecls
 
-let inductive_has_local_defs ind =
+let inductive_nrealdecls_env env ind =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_nrealdecls
+
+(* Full length of arity (w/o local defs) *)
+
+let inductive_nallargs ind =
   let (mib,mip) = Global.lookup_inductive ind in
-  let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealargs_ctxt in
-  let l2 = mib.mind_nparams + mip.mind_nrealargs in
-  not (Int.equal l1 l2)
+  mib.mind_nparams + mip.mind_nrealargs
+
+let inductive_nallargs_env env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mib.mind_nparams + mip.mind_nrealargs
 
 (* Length of arity (w/o local defs) *)
 
 let inductive_nparams ind =
-  (fst (Global.lookup_inductive ind)).mind_nparams
+  let (mib,mip) = Global.lookup_inductive ind in
+  mib.mind_nparams
+
+let inductive_nparams_env env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mib.mind_nparams
+
+(* Length of arity (with local defs) *)
+
+let inductive_nparamdecls ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  rel_context_length mib.mind_params_ctxt
+
+let inductive_nparamdecls_env env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  rel_context_length mib.mind_params_ctxt
+
+(* Full length of arity (with local defs) *)
+
+let inductive_nalldecls ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+
+let inductive_nalldecls_env env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
 
-let inductive_params_ctxt (ind,u) =
+(* Others *)
+
+let inductive_paramdecls (ind,u) =
   let (mib,mip) = Global.lookup_inductive ind in
-    Inductive.inductive_params_ctxt (mib,u)
+    Inductive.inductive_paramdecls (mib,u)
+
+let inductive_paramdecls_env env (ind,u) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+    Inductive.inductive_paramdecls (mib,u)
 
-let inductive_nargs ind =
+let inductive_alldecls (ind,u) =
   let (mib,mip) = Global.lookup_inductive ind in
-  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
+  let subst = Inductive.make_inductive_subst mib u in
+    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
 
-let inductive_nargs_env env ind =
+let inductive_alldecls_env env (ind,u) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
+  let subst = Inductive.make_inductive_subst mib u in
+    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
+
+let constructor_has_local_defs (indsp,j) =
+  let (mib,mip) = Global.lookup_inductive indsp in
+  let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
+  let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
+  not (Int.equal l1 l2)
+
+let inductive_has_local_defs ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
+  let l2 = mib.mind_nparams + mip.mind_nrealargs in
+  not (Int.equal l1 l2)
 
 let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -192,7 +265,7 @@ let allowed_sorts env (kn,i as ind) =
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
+  let print_info = { ind_nargs = mip.mind_nrealdecls; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1efc29c8f..10ff968cf 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -52,46 +52,70 @@ val mis_is_recursive :
 val mis_nf_constructor_type :
   pinductive * mutual_inductive_body * one_inductive_body -> int -> constr
 
-(** {6 Extract information from an inductive name}
+(** {6 Extract information from an inductive name} *)
 
+(** @return number of constructors *)
+val nconstructors : inductive -> int
+val nconstructors_env : env -> inductive -> int
 
-Functions without env lookup in the globalenv. *)
+(** @return arity of constructors excluding parameters, excluding local defs *)
+val constructors_nrealargs : inductive -> int array
+val constructors_nrealargs_env : env -> inductive -> int array
 
-(** Arity of constructors excluding parameters and local defs *)
-val mis_constr_nargs : inductive -> int array
-val mis_constr_nargs_env : env -> inductive -> int array
+(** @return arity of constructors excluding parameters, including local defs *)
+val constructors_nrealdecls : inductive -> int array
+val constructors_nrealdecls_env : env -> inductive -> int array
 
-val nconstructors : inductive -> int
+(** @return the arity, excluding params, including local defs *)
+val inductive_nrealdecls : inductive -> int
+val inductive_nrealdecls_env : env -> inductive -> 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 the arity, including params, excluding local defs *)
+val inductive_nallargs : inductive -> int
+val inductive_nallargs_env : env -> inductive -> int
 
-(** @return nb of params without letin *)
+(** @return the arity, including params, including local defs *)
+val inductive_nalldecls : inductive -> int
+val inductive_nalldecls_env : env -> inductive -> int
+
+(** @return nb of params without local defs *)
 val inductive_nparams : inductive -> int
-val inductive_params_ctxt : pinductive -> rel_context
+val inductive_nparams_env : env -> inductive -> int
+
+(** @return nb of params with local defs *)
+val inductive_nparamdecls : inductive -> int
+val inductive_nparamdecls_env : env -> inductive -> int
+
+(** @return params context *)
+val inductive_paramdecls : pinductive -> rel_context
+val inductive_paramdecls_env : env -> pinductive -> rel_context
+
+(** @return full arity context, hence with letin *)
+val inductive_alldecls : pinductive -> rel_context
+val inductive_alldecls_env : env -> pinductive -> rel_context
+
+(** {7 Extract information from a constructor name} *)
 
 (** @return param + args without letin *)
-val mis_constructor_nargs : constructor -> int
-val mis_constructor_nargs_env : env -> constructor -> int
+val constructor_nallargs : constructor -> int
+val constructor_nallargs_env : env -> constructor -> int
 
 (** @return param + args with letin *)
-val mis_constructor_nhyps : constructor -> int
-val mis_constructor_nhyps_env : env -> constructor -> int
+val constructor_nalldecls : constructor -> int
+val constructor_nalldecls_env : env -> constructor -> int
 
 (** @return args without letin *)
-val constructor_nrealargs : env -> constructor -> int
+val constructor_nrealargs : constructor -> int
+val constructor_nrealargs_env : env -> constructor -> int
 
 (** @return args with letin *)
-val constructor_nrealhyps : constructor -> int
+val constructor_nrealdecls : constructor -> int
+val constructor_nrealdecls_env : env -> constructor -> int
 
 (** Is there local defs in params or args ? *)
-val mis_constructor_has_local_defs : constructor -> bool
+val constructor_has_local_defs : constructor -> bool
 val inductive_has_local_defs : inductive -> bool
 
-val get_full_arity_sign : env -> pinductive -> rel_context
-
 val allowed_sorts : env -> inductive -> sorts_family list
 
 (** Extract information from an inductive family *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9609a959b..e5023e858 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -498,7 +498,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	Evarutil.evd_comb1 (Evd.fresh_inductive_instance env) evdref (mind,0)
       in
       let args = 
-	let ctx = smash_rel_context (Inductiveops.inductive_params_ctxt ind) in
+	let ctx = smash_rel_context (Inductiveops.inductive_paramdecls ind) in
 	  List.fold_right (fun (n, b, ty) (* par  *)args ->
 	    let ty = substl args ty in
 	    let ev = e_new_evar evdref env ~src:(loc,k) ty in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 669fbfb46..8f5a7e39a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -111,7 +111,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let p = pj.uj_val in
   let univ = e_is_correct_arity env evdref c pj ind specif params in
   let lc = build_branches_type ind specif params p in
-  let n = (snd specif).Declarations.mind_nrealargs_ctxt in
+  let n = (snd specif).Declarations.mind_nrealdecls in
   let ty =
     whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in
   (lc, ty, univ)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 7a536b35a..9cf2baf6f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -67,10 +67,10 @@ let with_context_set ctx (b, ctx') =
   (b, Univ.ContextSet.union ctx ctx')
 
 let build_dependent_inductive ind (mib,mip) =
-  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
+       extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
        @ extended_rel_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
@@ -104,7 +104,7 @@ let get_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let subst = Inductive.make_inductive_subst mib u in
   let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
-  let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
@@ -140,7 +140,7 @@ let get_non_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let subst = Inductive.make_inductive_subst mib u in
   let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
-  let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
@@ -737,7 +737,7 @@ let build_congr env (eq,refl,ctx) ind =
   let i = 1 in
   let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
   let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in
-  let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
@@ -769,12 +769,12 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        extended_rel_list (2*mip.mind_nrealargs_ctxt+3)
+	        extended_rel_list (2*mip.mind_nrealdecls+3)
 		  paramsctxt
 	        @ extended_rel_list 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
-                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) b|]);
+                mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
 		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
        mkVar varH,
        [|mkApp (refl,
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 63bb84613..e3ea08656 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -634,7 +634,7 @@ let find_positions env sigma t1 t2 =
     let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
       | Construct (sp1,_), Construct (sp2,_)
-          when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1)
+          when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
 	  let sorts' =
             Sorts.List.intersect sorts (allowed_sorts env (fst sp1))
@@ -642,7 +642,7 @@ let find_positions env sigma t1 t2 =
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if eq_constructor sp1 sp2 then
-	    let nrealargs = constructor_nrealargs env sp1 in
+	    let nrealargs = constructor_nrealargs_env env sp1 in
 	    let rargs1 = List.lastn nrealargs args1 in
 	    let rargs2 = List.lastn nrealargs args2 in
             List.flatten
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index a8bcec288..dc78229f6 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -159,7 +159,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
   let (hdapp,args) = decompose_app t in
   let res = match kind_of_term hdapp with
   | Ind (ind,u)  ->
-      let car = mis_constr_nargs ind in
+      let car = constructors_nrealargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
       if Array.for_all (fun ar -> Int.equal ar 1) car
 	&& not (mis_is_recursive (ind,mib,mip))
@@ -277,7 +277,7 @@ let match_with_equation t =
 let is_inductive_equality ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let nconstr = Array.length mip.mind_consnames in
-  Int.equal nconstr 1 && Int.equal (constructor_nrealargs (Global.env()) (ind,1)) 0
+  Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
 
 let match_with_equality_type t =
   let (hdapp,args) = decompose_app t in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bf64e15e9..07ac0ba9f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1033,7 +1033,7 @@ let descend_in_conjunctions tac exit c gl =
     let sign,ccl = decompose_prod_assum t in
     match match_with_tuple ccl with
     | Some (_,_,isrec) ->
-	let n = (mis_constr_nargs ind).(0) in
+	let n = (constructors_nrealargs ind).(0) in
 	let sort = elimination_sort_of_goal gl in
 	let id = fresh_id [] (Id.of_string "H") gl in
 	let IndType (indf,_) = pf_apply find_rectype gl ccl in
@@ -1485,7 +1485,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   let c = mkVar id in
   let t = Tacmach.New.pf_type_of gl c in
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let nv = mis_constr_nargs ind in
+  let nv = constructors_nrealargs ind in
   let ll = fix_empty_or_and_pattern (Array.length nv) ll in
   check_or_and_pattern_size loc ll (Array.length nv);
   Tacticals.New.tclTHENLASTn