Merge PR #11045: Forbid Include inside sections

Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot

2 files changed, 17 insertions, 0 deletions

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)