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

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9c83ba1a98..89d2d7b671 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;