Merge PR #8995: Don't redeclare constraints of fields in Include

3 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh
new file mode 100755
index 0000000000..96bdee2fc2
--- /dev/null
+++ b/test-suite/misc/quick-include.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+set -e
+
+$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v
+$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v
diff --git a/test-suite/misc/quick-include/file1.v b/test-suite/misc/quick-include/file1.v
new file mode 100644
index 0000000000..fa48e240cb
--- /dev/null
+++ b/test-suite/misc/quick-include/file1.v
@@ -0,0 +1,18 @@
+
+Module Type E. End E.
+
+Module M.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End M.
+
+
+Module Type T.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End T.
+
+Module F(A:E).
+  Lemma x : True.
+  Proof. trivial. Qed.
+End F.
diff --git a/test-suite/misc/quick-include/file2.v b/test-suite/misc/quick-include/file2.v
new file mode 100644
index 0000000000..ab10dfd8de
--- /dev/null
+++ b/test-suite/misc/quick-include/file2.v
@@ -0,0 +1,6 @@
+
+From QuickInclude Require file1.
+
+Module M. Include file1.M. End M.
+Module T. Include file1.T. End T.
+Module F. Include file1.F. End F.