From f0ef2d764673670fef52873c441bbbb2f1f7a34d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Mar 2020 19:24:53 +0100
Subject: Remove a useless reversed variant in Vars.

---
 kernel/vars.ml     | 3 ---
 kernel/vars.mli    | 3 ---
 pretyping/vnorm.ml | 2 +-
 3 files changed, 1 insertion(+), 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
 
 
-- 
cgit v1.2.3