From c4e2cf027b3fade4f9c2806e6061e1294a99e540 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Nov 2015 21:17:59 +0100
Subject: Fixing a vm_compute bug in the presence of let-ins among the
 parameters of an inductive type.

---
 pretyping/vnorm.ml          | 9 +++++----
 test-suite/success/Case22.v | 8 ++++++++
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c4c85a62ed..be772a6677 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -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
 
 
 
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index f88051f8f5..3c696502cd 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -53,3 +53,11 @@ Check fun x:Ind bool nat =>
   match x in Ind _ X Y Z return Z with
   | Constr _ => (true,0)
   end.
+
+(* A vm_compute bug (the type of constructors was not supposed to
+   contain local definitions before proper parameters) *)
+
+Inductive Ind2 (b:=1) (c:nat) : Type :=
+  Constr2 : Ind2 c.
+
+Eval vm_compute in Constr2 2.
-- 
cgit v1.2.3