diff options
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) |