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

7 files changed, 67 insertions, 16 deletions

diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index da098a420..aafbbf2a1 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -52,8 +52,8 @@ Module Check_Pair [X:PO][Y:PO] : PO := (Pair X Y).
 
 
 Module Type Fmono.
-  Module X:PO.
-  Module Y:PO.
+  Declare Module X:PO.
+  Declare Module Y:PO.
 
   Parameter f : X.T -> Y.T.
   
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
index 61f720179..94c344bbd 100644
--- a/test-suite/modules/ind.v
+++ b/test-suite/modules/ind.v
@@ -1,6 +1,6 @@
 Module Type SIG.
   Inductive w:Set:=A:w.
-  Definition f : w->w.
+  Parameter f : w->w.
 End SIG.
 
 Module M:SIG.
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
new file mode 100644
index 000000000..b2a103a8f
--- /dev/null
+++ b/test-suite/modules/mod_decl.v
@@ -0,0 +1,55 @@
+Module Type SIG.
+  Definition A:Set. (*error*)
+  Axiom A:Set.
+End SIG.
+
+Module M0.
+  Definition A:Set.
+  Exact nat.
+  Save.
+End M0.
+
+Module M1:SIG.
+  Definition A:=nat.
+End M1.
+
+Module M2<:SIG.
+  Definition A:=nat.
+End M2.
+
+Module M3:=M0.
+
+Module M4:SIG:=M0.
+
+Module M5<:SIG:=M0.
+
+
+Module F[X:SIG]:=X.
+
+
+Declare Module M6.
+
+
+Module Type T.
+
+  Declare Module M0.
+    Lemma A:Set (*error*).
+    Axiom A:Set.
+  End M0.
+  
+  Declare Module M1:SIG.
+  
+  Declare Module M2<:SIG.
+    Definition A:=nat.
+  End M2.
+  
+  Declare Module M3:=M0.
+  
+  Declare Module M4:SIG:=M0.  (* error *)
+  
+  Declare Module M5<:SIG:=M0.
+
+  Declare Module M6:=F M0.
+
+  Module M7.
+End T.
\ No newline at end of file
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.
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
index c2d1c52dd..418ece442 100644
--- a/test-suite/modules/objects.v
+++ b/test-suite/modules/objects.v
@@ -1,5 +1,3 @@
-Reset Initial.
-
 Module Type SET.
   Axiom T:Set.
   Axiom x:T.
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index d6ba0ae08..eb8736bba 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -1,7 +1,7 @@
 Module M.
   Module Type SIG.
-    Definition T:Set.
-    Definition x:T.
+    Parameter T:Set.
+    Parameter x:T.
   End SIG.
   Module N:SIG.
     Definition T:=nat.
@@ -12,9 +12,9 @@ End M.
 Module N:=M.
 
 Module Type SPRYT.
-  Module N.
+  Declare Module N.
     Definition T:=M.N.T.
-    Definition x:T.
+    Parameter x:T.
   End N.
 End SPRYT.
 
@@ -23,7 +23,7 @@ Module K':SPRYT:=M.
 
 Module Type SIG.
   Definition T:Set:=M.N.T.
-  Definition x:T.
+  Parameter x:T.
 End SIG.
 
 Module J:SIG:=M.N.
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 2dbac3407..1bd4faef0 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -1,5 +1,3 @@
-Reset Initial.
-
 Set Implicit Arguments.