1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
new file mode 100644
index 00000000..418ece44
--- /dev/null
+++ b/test-suite/modules/objects.v
@@ -0,0 +1,33 @@
+Module Type SET.
+  Axiom T:Set.
+  Axiom x:T.
+End SET.
+ 
+Implicit Arguments On.
+
+Module M[X:SET].
+  Definition T := nat.
+  Definition x := O.
+  Definition f := [A:Set][x:A]X.x.
+End M.
+
+Module N:=M.
+
+Module Nat.
+  Definition T := nat.
+  Definition x := O.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.f O).
+
+Module P[Y:SET] := N.
+
+Module Y:=P Z Nat.
+
+Check (Y.f O).
+
+
+
+