From 190c44d0b5c51d1911b9a0ce5e250590647b6989 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Sep 2018 15:46:19 +0200
Subject: Don't redeclare constraints of fields in Include

---
 kernel/safe_typing.ml | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index df10398b2f..73d18e835e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -496,7 +496,7 @@ type generic_name =
   | M (** name already known, cf the mod_mp field *)
   | MT (** name already known, cf the mod_mp field *)
 
-let add_field ((l,sfb) as field) gn senv =
+let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
   let mlabs,olabs = match sfb with
     | SFBmind mib ->
       let l = labels_of_mib mib in
@@ -506,8 +506,18 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let cst = constraints_of_sfb senv.env sfb in
-  let senv = add_constraints_list cst senv in
+  let senv =
+    if is_include then
+      (* Universes and constraints were added when the included module
+         was defined eg in [Include F X.] (one of the trickier
+         versions of Include) the constraints on the fields are
+         exactly those of the fields of F which was defined
+         separately. *)
+      senv
+    else
+      let cst = constraints_of_sfb senv.env sfb in
+      add_constraints_list cst senv
+  in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
     | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -1047,7 +1057,7 @@ let add_include me is_module inl senv =
       | SFBmodule _ -> M
       | SFBmodtype _ -> MT
     in
-    add_field field new_name senv
+    add_field ~is_include:true field new_name senv
   in
   resolver, List.fold_left add senv str
 
-- 
cgit v1.2.3


From 798e84b3313bd1e4b0f4937f31d4c570d2fa737f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 14 Nov 2018 13:02:06 +0100
Subject: Add test for Include in -quick mode

---
 test-suite/misc/quick-include.sh      |  5 +++++
 test-suite/misc/quick-include/file1.v | 18 ++++++++++++++++++
 test-suite/misc/quick-include/file2.v |  6 ++++++
 3 files changed, 29 insertions(+)
 create mode 100755 test-suite/misc/quick-include.sh
 create mode 100644 test-suite/misc/quick-include/file1.v
 create mode 100644 test-suite/misc/quick-include/file2.v

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.
-- 
cgit v1.2.3