From a3848b0a10064fb7e206a503ac8b829cb9ce4666 Mon Sep 17 00:00:00 2001
From: coq
Date: Tue, 13 Aug 2002 14:44:24 +0000
Subject: Petites corrections ici et la

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/modules/fun_objects.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'test-suite/modules/fun_objects.v')

diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
index b14c3f7935..0f8eef847c 100644
--- a/test-suite/modules/fun_objects.v
+++ b/test-suite/modules/fun_objects.v
@@ -1,29 +1,29 @@
 Implicit Arguments On.
 
-Modtype SIG.
+Module Type SIG.
   Parameter id:(A:Set)A->A.
-EndT SIG.
+End SIG.
  
-Mod M[X:SIG].
+Module M[X:SIG].
   Definition idid := (X.id X.id).
   Definition id := (idid X.id).
-EndM M.
+End M.
 
-Mod N:=M.
+Module N:=M.
 
-Mod Nat.
+Module Nat.
   Definition T := nat.
   Definition x := O.
   Definition id := [A:Set][x:A]x.
-EndM Nat.
+End Nat.
 
-Mod Z:=(N Nat).
+Module Z:=(N Nat).
 
 Check (Z.idid O).
 
-Mod P[Y:SIG] := N.
+Module P[Y:SIG] := N.
 
-Mod Y:=P Nat Z.
+Module Y:=P Nat Z.
 
 Check (Y.id O).
 
-- 
cgit v1.2.3