From f8a5cb590352a617de38fdd8ba5ffff7691d9841 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 15:17:28 +0200
Subject: Disallow dependent case on prim records w/o eta

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

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index b5e6ccd618..473d37eb36 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,7 +47,9 @@ Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
 Proof. Fail reflexivity. Abort.
 
+Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }.
 
+Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.
-- 
cgit v1.2.3