2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v
new file mode 100644
index 000000000..74c8fa347
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2668.v
@@ -0,0 +1,6 @@
+Require Import MSetPositive.
+Require Import MSetProperties.
+
+Module Pos := MSetPositive.PositiveSet.
+Module PPPP := MSetProperties.WPropertiesOn(Pos).
+Print Module PPPP.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v
new file mode 100644
index 000000000..15598352b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2983.v
@@ -0,0 +1,8 @@
+Module Type ModA.
+End ModA.
+Module Type ModB(A : ModA).
+End ModB.
+Module Foo(A : ModA)(B : ModB A).
+End Foo.
+
+Print Module Foo.
+\ No newline at end of file