diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 21:17:59 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 21:55:21 +0100 |
commit | c4e2cf027b3fade4f9c2806e6061e1294a99e540 (patch) | |
tree | 62d861dbc2e3e2f94c82fd4d0b35d52b84b4442e /pretyping/vnorm.ml | |
parent | af954522789043202d9c300a0bb37cbaf4958d60 (diff) |
Fixing a vm_compute bug in the presence of let-ins among the
parameters of an inductive type.
Diffstat (limited to 'pretyping/vnorm.ml')
-rw-r--r-- | pretyping/vnorm.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c4c85a62e..be772a667 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -59,11 +59,12 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let nparams = Array.length params in - if Int.equal nparams 0 then ctyp + let ndecls = Context.rel_context_length mib.mind_params_ctxt in + if Int.equal ndecls 0 then ctyp else - let _,ctyp = decompose_prod_n nparams ctyp in - substl (Array.rev_to_list params) ctyp + let _,ctyp = decompose_prod_n_assum ndecls ctyp in + substl (List.rev (Termops.adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + ctyp |