2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3804.v b/test-suite/bugs/opened/3804.v
new file mode 100644
index 000000000..4c7f9344e
--- /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 000000000..df40ca191
--- /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.