1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3670.v b/test-suite/bugs/closed/3670.v
new file mode 100644
index 00000000..c0f03261
--- /dev/null
+++ b/test-suite/bugs/closed/3670.v
@@ -0,0 +1,23 @@
+Set Universe Polymorphism.
+Module Type FOO.
+  Parameter f : Type -> Type.
+  Parameter h : forall T, f T.
+End FOO.
+
+Module Type BAR.
+  Include FOO.
+End BAR.
+
+Module Type BAZ.
+  Include FOO.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) <: BAR.
+
+  Definition f : Type -> Type. 
+  Proof. exact baz.f. Defined.
+
+  Definition h : forall T, f T.
+  Admitted.
+
+Fail End BAR_FROM_BAZ.