1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
new file mode 100644
index 00000000..2231e084
--- /dev/null
+++ b/test-suite/modules/obj.v
@@ -0,0 +1,26 @@
+Implicit Arguments On.
+
+Module M. 
+  Definition a:=[s:Set]s.
+  Print a.
+End M.
+
+Print M.a.
+
+Module K.
+  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+  Module N.
+    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+    Print app.
+    Print apap.
+  End N.
+  Print N.apap.
+End K.
+
+Print K.app.
+Print K.N.apap.
+
+Module W:=K.N.
+
+Print W.apap.
+