From cb145fa37d463210832c437f013231c9f028e1aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 Jul 2015 13:58:05 +0200
Subject: Output test for bug #2169.

---
 test-suite/output/PrintModule.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/output/PrintModule.v

(limited to 'test-suite/output/PrintModule.v')

diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
new file mode 100644
index 0000000000..999d9a9862
--- /dev/null
+++ b/test-suite/output/PrintModule.v
@@ -0,0 +1,34 @@
+Module FOO.
+
+Module M.
+ Definition T := nat.
+End M.
+
+Module Type S.
+ Parameter T : Set.
+End S.
+
+Module N : S with Definition T := nat := M.
+
+Print Module N.
+
+End FOO.
+
+Module BAR.
+
+Module K. End K.
+Module Type KS. End KS.
+
+Module M.
+ Module T := K.
+End M.
+
+Module Type S.
+ Declare Module T : KS.
+End S.
+
+Module N : S with Module T := K := M.
+
+Print Module N.
+
+End BAR.
-- 
cgit v1.2.3