From 03472e2da94043fa35a618e92191b63fbe4c196d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Dec 2005 23:22:00 +0000
Subject: 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
---
 test-suite/modules/mod_decl.v | 18 ++++++------------
 test-suite/modules/modeq.v    |  2 +-
 test-suite/modules/modul.v    |  8 +++-----
 test-suite/modules/sig.v      |  2 +-
 4 files changed, 11 insertions(+), 19 deletions(-)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index 867b8a11fb..a9d22d79d8 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 73448dc7fe..9e74a310d1 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 5612ea7553..58ae2a52df 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 eb8736bbac..c09a743241 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.
-- 
cgit v1.2.3