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

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