diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-19 22:49:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:14 +0100 |
| commit | ade2363e357db3ac3f258e645fe6bba988e7e7dd (patch) | |
| tree | ade794510151d080d164be6d33d03aacbbe5064f /pretyping/vnorm.ml | |
| parent | f66e604a9d714ee9dba09234d935ee208bc89d97 (diff) | |
About building of substitutions from instances.
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
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 |