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).

1 files changed, 1 insertions, 15 deletions

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb..b5e6ccd61 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.
 
 
 (*