diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 60140a31d..c59e085e5 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -57,7 +57,7 @@ let type_constructor mind mib u typ params = if Int.equal ndecls 0 then ctyp else 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))) + substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) ctyp |