From e583a79b5a0298fd08f34305cc876d5117913e95 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:23:12 +0100
Subject: Fixing kernel bug in typing match with let-ins in the arity.

Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).

Fixing similar error in pretyping.
---
 test-suite/success/Case22.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index ce9050d421..8c8f02eccf 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -17,3 +17,27 @@ Definition foo (x : I') : bool :=
   match x with
   C' => true
   end.
+
+(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)
+
+Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
+  E2 : I2 A nat.
+
+Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
+  E2 _ => (0,0,(0,0))
+  end.
+
+(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
+
+Inductive IND : forall X:Type, let Y:=X in Type :=
+  C : IND True.
+
+Definition F (x:IND True) (A:Type) :=
+  (* This failed in 8.5beta2 though it should have been accepted *)
+  match x in IND Y Z return Z with
+  C => I
+  end.
+
+Theorem paradox : False.
+  (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
+Fail Proof (F C False).
-- 
cgit v1.2.3


From af954522789043202d9c300a0bb37cbaf4958d60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Nov 2015 17:17:49 +0100
Subject: Fixing a bug of adjust_subst_to_rel_context.

---
 test-suite/success/Case22.v | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 8c8f02eccf..f88051f8f5 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -30,14 +30,26 @@ Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
 (* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
 
 Inductive IND : forall X:Type, let Y:=X in Type :=
-  C : IND True.
+  CONSTR : IND True.
 
 Definition F (x:IND True) (A:Type) :=
   (* This failed in 8.5beta2 though it should have been accepted *)
-  match x in IND Y Z return Z with
-  C => I
+  match x in IND X Y return Y with
+  CONSTR => Logic.I
   end.
 
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+
+(* Another bug found in November 2015 (a substitution was wrongly
+   reversed at pretyping level) *)
+
+Inductive Ind (A:Type) :
+  let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type :=
+  Constr : Ind A nat.
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | Constr _ => (true,0)
+  end.
-- 
cgit v1.2.3


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.

---
 test-suite/success/Case22.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

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