MAJ syntaxe v7 avant activation en syntaxe v8

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

4 files changed, 11 insertions, 19 deletions

diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index 867b8a11f..a9d22d79d 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -1,5 +1,4 @@
 Module Type SIG.
-  Definition A:Set. (*error*)
   Axiom A:Set.
 End SIG.
 
@@ -27,13 +26,9 @@ Module M5<:SIG:=M0.
 Module F[X:SIG]:=X.
 
 
-Declare Module M6.
-
-
 Module Type T.
 
-  Declare Module M0.
-    Lemma A:Set (*error*).
+  Module M0.
     Axiom A:Set.
   End M0.
   
@@ -43,13 +38,12 @@ Module Type T.
     Definition A:=nat.
   End M2.
   
-  Declare Module M3:=M0.
+  Module M3:=M0.
   
-  Declare Module M4:SIG:=M0.  (* error *)
+  Module M4:SIG:=M0.
   
-  Declare Module M5<:SIG:=M0.
+  Module M5<:SIG:=M0.
 
-  Declare Module M6:=F M0. (* error *)
+  Module M6:=F M0.
 
-  Module M7.
-End T.
\ No newline at end of file
+End T.
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 73448dc7f..9e74a310d 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -4,7 +4,7 @@ Module M.
 End M.
 
 Module Type SIG.
-  Declare Module M:=Top.M.
+  Module M:=Top.M.
   Module Type SIG.
     Parameter T:Set.
   End SIG.
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 5612ea755..58ae2a52d 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -16,24 +16,22 @@ Module M.
 
 End M.
 
+Locate Module M.
+
 (*Lemma w1 : (M.rel O (S O)).
 Auto.
 *)
 
 Import M.
 
-Print Hint *.
 Lemma w1 : (O#(S O)).
-Print Hint.
-Print Hint *.
-
 Auto.
 Save.
 
 Check (O#O).
 Locate rel.
 
-Locate M.
+Locate Module M.
 
 Module N:=Top.M.
 
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index eb8736bba..c09a74324 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -12,7 +12,7 @@ End M.
 Module N:=M.
 
 Module Type SPRYT.
-  Declare Module N.
+  Module N.
     Definition T:=M.N.T.
     Parameter x:T.
   End N.