diff options
| author | Pierre-Marie Pédrot | 2020-03-28 19:24:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-28 19:26:06 +0100 |
| commit | f0ef2d764673670fef52873c441bbbb2f1f7a34d (patch) | |
| tree | 265fd4af6bd0e5190e4a2403a8be4f6b3652be41 /pretyping/vnorm.ml | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
Remove a useless reversed variant in Vars.
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 64068724af..d4da93cc5b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -73,7 +73,7 @@ let type_constructor mind mib u (ctx, typ) params = if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in - substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + substl (subst_of_rel_context_instance mib.mind_params_ctxt (Array.to_list params)) ctyp |