diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 106fed124e..9a1d935928 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1081,10 +1081,9 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) let warn_require_in_section = - let name = "require-in-section" in - let category = "deprecated" in - CWarnings.create ~name ~category - (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + CWarnings.create ~name:"require-in-section" ~category:"fragile" + (fun () -> strbrk "Use of “Require” inside a section is fragile." ++ spc() ++ + strbrk "It is not recommended to use this functionality in finished proof scripts.") let vernac_require from import qidl = if Global.sections_are_opened () then warn_require_in_section (); |