aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/modeq.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules/modeq.v')
-rw-r--r--test-suite/modules/modeq.v8
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.