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
---
 vernac/declaremods.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'vernac')

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