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.

---
 pretyping/vnorm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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