Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 35 insertions, 0 deletions

diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
new file mode 100644
index 000000000..f800dec52
--- /dev/null
+++ b/test-suite/modules/sub_objects.v
@@ -0,0 +1,35 @@
+Reset Initial.
+
+Set Implicit Arguments.
+
+
+Mod M.
+  Definition id:=[A:Set][x:A]x.
+
+  Modtype SIG.
+    Parameter idid:(A:Set)A->A.
+  EndT SIG.
+
+  Mod N.
+    Definition idid:=[A:Set][x:A](id x).
+    Grammar constr constr8 := 
+      not_eq [ "#"  constr7($b) ] -> [ (idid $b) ].
+    Syntactic Definition inc := (plus (S O)). 
+  EndM N.
+
+  Definition zero:=(N.idid O).
+
+EndM M.
+
+Definition zero := (M.N.idid O).
+Definition jeden := (M.N.inc O).
+
+Mod Goly:=M.N.
+
+Definition Gole_zero := (Goly.idid O).
+Definition Goly_jeden := (Goly.inc O).
+
+Mod Ubrany : M.SIG := M.N.
+
+Definition Ubrane_zero := (Ubrany.idid O).
+