diff options
| author | Pierre-Marie Pédrot | 2019-11-12 08:33:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-12 08:33:33 +0100 |
| commit | 2636d47bac7f31a5492100a4c13eb4fe4d932d1f (patch) | |
| tree | 9353e97ff5b4204da2a628ed683f6b5ebecea09c /vernac | |
| parent | 73821fcf0cb0b87b7cf339e93ff9a5020ddd2644 (diff) | |
| parent | bb39a0238ac341c407aef9ca8e8601c75789d3b5 (diff) | |
Merge PR #11045: Forbid Include inside sections
Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot
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) |