aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-17 12:17:01 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-17 13:48:18 +0200
commit159b10655172b6f0888f9622be3620c3c33d35b1 (patch)
treeadf94a1f8e742001ecf5d570d187b85f771851f1 /test-suite
parentfd39a2e844f93b314c2f0b78510f0573cfa1bef3 (diff)
Test for bug #4874.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/qualification.out3
-rw-r--r--test-suite/output/qualification.v19
2 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 000000000..3cf3c2d8f
--- /dev/null
+++ b/test-suite/output/qualification.out
@@ -0,0 +1,3 @@
+File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
+Error: Signature components for label test do not match: expected type
+"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
new file mode 100644
index 000000000..d39097e2d
--- /dev/null
+++ b/test-suite/output/qualification.v
@@ -0,0 +1,19 @@
+Module Type T1.
+ Parameter t : Type.
+End T1.
+
+Module Type T2.
+ Declare Module M : T1.
+ Parameter t : Type.
+ Parameter test : t = M.t.
+End T2.
+
+Module M1 <: T1.
+ Definition t : Type := bool.
+End M1.
+
+Module M2 <: T2.
+ Module M := M1.
+ Definition t : Type := nat.
+ Lemma test : t = t. Proof. reflexivity. Qed.
+End M2.