diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ea22c3708f..be2fd81290 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,6 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = + (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then @@ -521,6 +522,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin let num_cnstr_args = let nparamsctxt = + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) |