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

4 files changed, 6 insertions, 6 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 *)