From 1c186562c2fc628d9ec4b6cda888750a642da117 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 5 Jan 2015 16:33:20 +0100
Subject: kernel/ind Change interface of declare_mind and declare_mutual

Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
---
 test-suite/bugs/closed/3899.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3899.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3899.v b/test-suite/bugs/closed/3899.v
new file mode 100644
index 0000000000..e83166aaec
--- /dev/null
+++ b/test-suite/bugs/closed/3899.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+Record unit : Set := tt {}.
+Fail Check fun x : unit => eq_refl : tt = x.
+Fail Check fun x : unit => eq_refl : x = tt.
+Fail Check fun x y : unit => (eq_refl : x = tt) : x = y.
+Fail Check fun x y : unit => eq_refl : x = y.
+
+Record ok : Set := tt' { a : unit }.
+
+Record nonprim : Prop := { undef : unit }.
+Record prim : Prop := { def : True }.
\ No newline at end of file
-- 
cgit v1.2.3