diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-27 20:16:35 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:16 +0200 |
| commit | 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac (patch) | |
| tree | 916f61f35650966d7a288e8579279b0a3e45afc6 /pretyping/evarconv.ml | |
| parent | 7b5fcef8a0fb3b97a3980f10596137234061990f (diff) | |
Fix bugs and add an option for cumulativity
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 ea22c3708..be2fd8129 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) |