diff --git a/library/global.ml b/library/global.ml
index 6a45bb45cdfe8..d6170d6811726 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -20,6 +20,7 @@ module GlobalSafeEnv : sig
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
   val is_joined_environment : unit -> bool
+  val is_curmod_library : unit -> bool
   val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
@@ -30,6 +31,9 @@ let global_env, global_env_summary_tag =
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
 
+let is_curmod_library () =
+  Safe_typing.is_curmod_library !global_env
+
 let assert_not_synterp () =
   if !Flags.in_synterp_phase then
     CErrors.anomaly (
@@ -45,6 +49,7 @@ let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
 
 let safe_env = GlobalSafeEnv.safe_env
 let is_joined_environment = GlobalSafeEnv.is_joined_environment
+let is_curmod_library = GlobalSafeEnv.is_curmod_library
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 
diff --git a/library/global.mli b/library/global.mli
index 01b323810a972..98b93c985e723 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -152,6 +152,7 @@ val import :
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val is_joined_environment : unit -> bool
+val is_curmod_library : unit -> bool
 
 val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f6f903ceee033..128dca0d10c7c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -923,6 +923,9 @@ GRAMMAR EXTEND Gram
   command:
     [ [ IDENT "Comments"; l = LIST0 comment -> { VernacSynPure (VernacComments l) }
 
+      | IDENT "Library"; b = [ IDENT "Comment" -> { false } | IDENT "Warning" -> { true } ];
+        s = STRING -> { VernacSynPure (VernacLibraryComment (b, s)) }
+
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
       | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
          t = term LEVEL "200";
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 9fac3430ba2d4..70069163554b4 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1216,6 +1216,14 @@ let pr_synpure_vernac_expr v =
          ++ prlist_with_sep sep (pr_comment pr_constr) l)
     )
 
+  | VernacLibraryComment (warning,s) ->
+    return (
+      hov 2
+        (keyword "Library" ++ spc()
+         ++ keyword (if warning then "Warning" else "Comment") ++ spc ()
+         ++ qs s)
+    )
+
   | VernacProof (None, None) ->
     return (keyword "Proof")
   | VernacProof (None, Some e) ->
diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml
index 3d202c92fcc1b..9f09524cbce57 100644
--- a/vernac/vernac_classifier.ml
+++ b/vernac/vernac_classifier.ml
@@ -176,6 +176,7 @@ let classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _
+    | VernacLibraryComment _
     | VernacSchemeEquality _
     | VernacDeclareInstance _ -> VtSideff ([], VtLater)
     (* Who knows *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a7b53506cc978..7e2542767f12a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1399,7 +1399,11 @@ let vernac_require_interp needed modrefl export qidl =
   in
   if Dumpglob.dump () then
     List.iter2 (fun ({CAst.loc},_) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl modrefl;
+  (* Load *)
   Library.require_library_from_dirpath needed;
+  (* Output warnings of the file *)
+  Flags.if_verbose (List.iter (fun m -> Docstring.output_warnings_modpath (MPfile m))) modrefl;
+  (* Import*)
   Option.iter (fun (export,cats) ->
       let cats = interp_import_cats cats in
       List.iter2 (fun m (_,f) ->
@@ -2076,6 +2080,13 @@ let vernac_register qid r =
     end
     else Coqlib.register_ref (Libnames.string_of_qualid n) gr
 
+let vernac_library_comment warning comment =
+  if Global.is_curmod_library () && not (Lib.sections_are_opened ()) then
+    Docstring.declare_docstring_modpath (MPfile (Lib.library_dp ()))
+      { comment; warning }
+  else
+    user_err (Pp.str "A library comment should be at toplevel of the library.")
+
 (********************)
 (* Proof management *)
 
@@ -2499,6 +2510,11 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with
         unsupported_attributes atts;
         Flags.if_verbose Feedback.msg_info (str "Comments ok\n"))
 
+  | VernacLibraryComment (b,s) ->
+    vtdefault(fun () ->
+        unsupported_attributes atts;
+        vernac_library_comment b s)
+
   (* Proof management *)
   | VernacFocus n ->
     vtmodifyproof(unsupported_attributes atts;vernac_focus n)
diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli
index 579b4cfc50311..ddbeaf3a65ed6 100644
--- a/vernac/vernacexpr.mli
+++ b/vernac/vernacexpr.mli
@@ -472,6 +472,7 @@ type nonrec synpure_vernac_expr =
   | VernacRegister of qualid * register_kind
   | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option
   | VernacComments of comment list
+  | VernacLibraryComment of bool * string
 
   (* Proof management *)
   | VernacAbort