1 files changed, 6 insertions, 12 deletions
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.