Fixing a vm_compute bug in the presence of let-ins among the

parameters of an inductive type.

1 files changed, 8 insertions, 0 deletions

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.