summaryrefslogtreecommitdiff
path: root/test-suite/modules
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /test-suite/modules
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/mod_decl.v2
-rw-r--r--test-suite/modules/objects2.v11
2 files changed, 12 insertions, 1 deletions
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index aad493ce..b886eb59 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -34,7 +34,7 @@ Module Type T.
Declare Module M1: SIG.
- Declare Module M2 <: SIG.
+ Module M2 <: SIG.
Definition A := nat.
End M2.
diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v
new file mode 100644
index 00000000..e286609e
--- /dev/null
+++ b/test-suite/modules/objects2.v
@@ -0,0 +1,11 @@
+(* Check that non logical object loading is done after registration of
+ the logical objects in the environment
+*)
+
+(* Bug #1118 (simplified version), submitted by Evelyne Contejean
+ (used to failed in pre-V8.1 trunk because of a call to lookup_mind
+ for structure objects)
+*)
+
+Module Type S. Record t : Set := { a : nat; b : nat }. End S.
+Module Make (X:S). Module Y:=X. End Make.