From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 10 Mar 2016 19:02:16 +0100
Subject: Primitive projections: protect kernel from erroneous definitions.

E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.

- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
  must be strictly non recursive for BiFinite declarations).
---
 test-suite/success/primitiveproj.v | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb3..b5e6ccd618 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
 
 Check nat.
 
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
 Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
 
 Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
 
 Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y := 
-  match n with
-    | 0 => t
-    | S n => {| next := Some (yn n y) |}
-  end.
+Proof. Fail reflexivity. Abort.
 
-Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
 
 
 (* 
-- 
cgit v1.2.3


From e9bf68016ce9e04feb63222ff4bbafd27531f564 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 11 Mar 2016 10:32:14 +0100
Subject: According to Bruno, my fix for #4588 seems to be enough.

So adding a test-suite file and closing the bug.
---
 test-suite/bugs/closed/4588.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/4588.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v
new file mode 100644
index 0000000000..ff66277e03
--- /dev/null
+++ b/test-suite/bugs/closed/4588.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+(* This proof was accepted in Coq 8.5 because the subterm specs were not
+projected correctly *)
+Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }.
+
+Fail Fixpoint loop (x : foo) : False :=
+  loop (proj2 x _ x).
+
+Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
-- 
cgit v1.2.3


From 779fd5d9a4982b19fd257b61f444ae8e6155dcbe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 19:50:29 +0100
Subject: Fix bug when a sort is ascribed to a Record

Forcefully equating it to the inferred level is not always desirable or possible.
---
 test-suite/success/univers.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb68..269359ae62 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
 (* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
 
 Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+  myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+  BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec.
\ No newline at end of file
-- 
cgit v1.2.3