diff options
| -rw-r--r-- | kernel/vars.ml | 3 | ||||
| -rw-r--r-- | kernel/vars.mli | 3 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
3 files changed, 1 insertions, 7 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 4c66f1574f..a4465c293b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -169,9 +169,6 @@ let subst_of_rel_context_instance sign l = | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l -let adjust_subst_to_rel_context sign l = - List.rev (subst_of_rel_context_instance sign l) - let adjust_rel_to_rel_context sign n = let rec aux sign = let open RelDecl in diff --git a/kernel/vars.mli b/kernel/vars.mli index 52a6159f0a..0aac5ed4ce 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -72,9 +72,6 @@ type substl = constr list [c₁], as if usable for [substl]. *) val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl -(** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list - (** Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int 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 |