From 91e01278de2420a64f1c8de03c0bc6e614577042 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 18:53:35 +0200
Subject: Univs: fixed bug #4328.

---
 test-suite/bugs/closed/4328.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4328.v

diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v
new file mode 100644
index 0000000000..8e1bb31007
--- /dev/null
+++ b/test-suite/bugs/closed/4328.v
@@ -0,0 +1,6 @@
+Inductive M (A:Type) : Type := M'.
+Axiom pi : forall (P : Prop) (p : P), Prop.
+Definition test1 A (x : _) := pi A x.           (* success     *)
+Fail Definition test2 A (x : A) := pi A x.           (* failure ??? *)
+Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure     *)
+Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file
-- 
cgit v1.2.3