1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3804.v b/test-suite/bugs/closed/3804.v
new file mode 100644
index 0000000000..5dc0f72642
--- /dev/null
+++ b/test-suite/bugs/closed/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.
+Definition foo := eq_refl : Foo.T = Bar.T. (* Error: Conversion test raised an anomaly *)
+\ No newline at end of file