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

1 files changed, 7 insertions, 7 deletions

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,