From f43c3bc3165567173c86d5f425fb834018c22a1b Mon Sep 17 00:00:00 2001
From: Xavier Clerc
Date: Fri, 14 Nov 2014 16:29:42 +0100
Subject: Reproduction cases for the test suite.

---
 test-suite/bugs/opened/3804.v | 12 ++++++++++++
 test-suite/bugs/opened/3808.v |  2 ++
 2 files changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/opened/3804.v
 create mode 100644 test-suite/bugs/opened/3808.v

diff --git a/test-suite/bugs/opened/3804.v b/test-suite/bugs/opened/3804.v
new file mode 100644
index 0000000000..4c7f9344e4
--- /dev/null
+++ b/test-suite/bugs/opened/3804.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+Module Foo.
+  Definition T : sigT (fun x => x).
+  Proof.
+    exists Set.
+    abstract exact nat.
+  Defined.
+End Foo.
+Module Bar.
+  Include Foo.
+End Bar.
+Fail Definition foo := eq_refl : Foo.T = Bar.T.
diff --git a/test-suite/bugs/opened/3808.v b/test-suite/bugs/opened/3808.v
new file mode 100644
index 0000000000..df40ca1910
--- /dev/null
+++ b/test-suite/bugs/opened/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
-- 
cgit v1.2.3