diff options
| author | Gaëtan Gilbert | 2019-11-04 16:46:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-05 14:04:06 +0100 |
| commit | bb39a0238ac341c407aef9ca8e8601c75789d3b5 (patch) | |
| tree | be822a7d71cf3317ef4f0013ad8c691176684951 /vernac | |
| parent | 634cb7b8a07a34fc29d074591091f0a6170f7bff (diff) | |
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
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declaremods.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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) |