diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_10060.v | 15 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 2 |
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) |