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

5 files changed, 12 insertions, 12 deletions

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