MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout

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

1 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 380716853..73448dc7f 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -4,17 +4,17 @@ Module M.
 End M.
 
 Module Type SIG.
-  Module M:=Top.M.
+  Declare Module M:=Top.M.
   Module Type SIG.
-    Definition T:Set.
+    Parameter T:Set.
   End SIG.
-  Module N:SIG.
+  Declare Module N:SIG.
 End SIG.
 
 Module Z.
   Module M:=Top.M.
   Module Type SIG.
-    Definition T:Set.
+    Parameter T:Set.
   End SIG.
   Module N:=M.
 End Z.