From bb39a0238ac341c407aef9ca8e8601c75789d3b5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 4 Nov 2019 16:46:55 +0100
Subject: Forbid Include inside sections

This probably does not work well in general, and specifically avoids
an anomaly fixing https://github.com/coq/coq/issues/10060
---
 test-suite/bugs/closed/bug_10060.v | 15 +++++++++++++++
 vernac/declaremods.ml              |  2 ++
 2 files changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10060.v

diff --git a/test-suite/bugs/closed/bug_10060.v b/test-suite/bugs/closed/bug_10060.v
new file mode 100644
index 0000000000..d74f6e388b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10060.v
@@ -0,0 +1,15 @@
+Module Type T.
+  Parameter b : Set.
+End T.
+
+Module M1(N : T).
+End M1.
+
+Module M2.
+End M2.
+
+Section S.
+  Variable a : Set.
+  Definition b := a.
+  Fail Include M1.
+End S.
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 65cd4cd6a4..54dda09e83 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -972,6 +972,8 @@ let declare_modtype id args mtys mty_l =
   protect_summaries declare_mt
 
 let declare_include me_asts =
+  if Global.sections_are_opened () then
+    user_err Pp.(str "Include is not allowed inside sections.");
   protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts)
 
 
-- 
cgit v1.2.3