From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 pretyping/vnorm.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping/vnorm.ml')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c4c85a62..7d86fad9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -59,11 +59,12 @@ let type_constructor mind mib u typ params =
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let ctyp = subst_instance_constr u ctyp in
-  let nparams = Array.length params in
-  if Int.equal nparams 0 then ctyp
+  let ndecls = Context.rel_context_length mib.mind_params_ctxt in
+  if Int.equal ndecls 0 then ctyp
   else
-    let _,ctyp = decompose_prod_n nparams ctyp in
-    substl (Array.rev_to_list params) ctyp
+    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)))
+      ctyp
 
 
 
-- 
cgit v1.2.3