aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/PO.v4
-rw-r--r--test-suite/modules/ind.v2
-rw-r--r--test-suite/modules/mod_decl.v55
-rw-r--r--test-suite/modules/modeq.v8
-rw-r--r--test-suite/modules/objects.v2
-rw-r--r--test-suite/modules/sig.v10
-rw-r--r--test-suite/modules/sub_objects.v2
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.