From 159b10655172b6f0888f9622be3620c3c33d35b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 12:17:01 +0200
Subject: Test for bug #4874.

---
 test-suite/output/qualification.out |  3 +++
 test-suite/output/qualification.v   | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 test-suite/output/qualification.out
 create mode 100644 test-suite/output/qualification.v

(limited to 'test-suite')

diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 0000000000..3cf3c2d8fb
--- /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 0000000000..d39097e2dd
--- /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.
-- 
cgit v1.2.3