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 0000000000..b02bdf189d
--- /dev/null
+++ b/test-suite/modules/obj.v
@@ -0,0 +1,26 @@
+Implicit Arguments On.
+
+Mod M. 
+  Definition a:=[s:Set]s.
+  Print a.
+EndM M.
+
+Print M.a.
+
+Mod K.
+  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+  Mod N.
+    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+    Print app.
+    Print apap.
+  EndM N.
+  Print N.apap.
+EndM K.
+
+Print K.app.
+Print K.N.apap.
+
+Mod W:=K.N.
+
+Print W.apap.
+