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, 13 insertions, 13 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 7a536b35aa..9cf2baf6f8 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 63bb846139..e3ea08656a 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 a8bcec2881..dc78229f68 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 bf64e15e93..07ac0ba9f2 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