diff options
| author | coq | 2002-08-13 14:44:24 +0000 |
|---|---|---|
| committer | coq | 2002-08-13 14:44:24 +0000 |
| commit | a3848b0a10064fb7e206a503ac8b829cb9ce4666 (patch) | |
| tree | 57715eb46564f71b91825c46ecb432a41c1ec095 /test-suite/modules/objects.v | |
| parent | bc4e7b8c2317b2536eb42efb7cbf37d748ceb7c6 (diff) | |
Petites corrections ici et la
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/modules/objects.v')
| -rw-r--r-- | test-suite/modules/objects.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v index 8183c67c68..c2d1c52dd9 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -1,32 +1,32 @@ Reset Initial. -Modtype SET. +Module Type SET. Axiom T:Set. Axiom x:T. -EndT SET. +End SET. Implicit Arguments On. -Mod M[X:SET]. +Module M[X:SET]. Definition T := nat. Definition x := O. Definition f := [A:Set][x:A]X.x. -EndM M. +End M. -Mod N:=M. +Module N:=M. -Mod Nat. +Module Nat. Definition T := nat. Definition x := O. -EndM Nat. +End Nat. -Mod Z:=(N Nat). +Module Z:=(N Nat). Check (Z.f O). -Mod P[Y:SET] := N. +Module P[Y:SET] := N. -Mod Y:=P Z Nat. +Module Y:=P Z Nat. Check (Y.f O). |