diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
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; |