Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
new file mode 100644
index 00000000..0f8eef84
--- /dev/null
+++ b/test-suite/modules/fun_objects.v
@@ -0,0 +1,32 @@
+Implicit Arguments On.
+
+Module Type SIG.
+  Parameter id:(A:Set)A->A.
+End SIG.
+ 
+Module M[X:SIG].
+  Definition idid := (X.id X.id).
+  Definition id := (idid X.id).
+End M.
+
+Module N:=M.
+
+Module Nat.
+  Definition T := nat.
+  Definition x := O.
+  Definition id := [A:Set][x:A]x.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.idid O).
+
+Module P[Y:SIG] := N.
+
+Module Y:=P Nat Z.
+
+Check (Y.id O).
+
+
+
+