Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.

10 files changed, 28 insertions, 19 deletions

diff --git a/library/coqlib.mli b/library/coqlib.mli
index 351a0a7e84..f6779dbbde 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -190,12 +190,18 @@ val build_bool_type : coq_bool_data delayed
 val build_prod : coq_sigma_data delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
-val build_coq_eq       : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq       : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_refl  : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *)
+(** = [(build_coq_eq_data()).eq] *)
+
+val build_coq_eq_refl  : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_sym   : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *)
+(** = [(build_coq_eq_data()).refl] *)
+
+val build_coq_eq_sym   : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
+(** = [(build_coq_eq_data()).sym] *)
+
 val build_coq_f_equal2 : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
@@ -222,8 +228,8 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 val build_coq_sumbool : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
-(** {6 ... } *)
-(** Connectives
+(** {6 ... }
+   Connectives
    The False proposition *)
 val build_coq_False : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
diff --git a/library/decls.mli b/library/decls.mli
index 401884736e..c0db537427 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (** opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
diff --git a/library/goptions.ml b/library/goptions.ml
index 98efb512ab..340d74151b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -246,14 +246,14 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
       | OptGlobal -> cache_options o
       | OptExport -> ()
       | OptLocal | OptDefault ->
-        (** Ruled out by classify_function *)
+        (* Ruled out by classify_function *)
         assert false
       in
       let open_options i  (_, (l, _, _) as o) = match l with
       | OptExport -> if Int.equal i 1 then cache_options o
       | OptGlobal -> ()
       | OptLocal | OptDefault ->
-        (** Ruled out by classify_function *)
+        (* Ruled out by classify_function *)
         assert false
       in
       let subst_options (subst,obj) = obj in
diff --git a/library/lib.ml b/library/lib.ml
index 9c13cdafdb..cce5feeb4a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -481,8 +481,8 @@ let named_of_variable_context =
   List.map fst
 
 let name_instance inst =
-  (** FIXME: this should probably be done at an upper level, by storing the
-      name information in the section data structure. *)
+  (* FIXME: this should probably be done at an upper level, by storing the
+     name information in the section data structure. *)
   let map lvl = match Univ.Level.name lvl with
     | None -> (* Having Prop/Set/Var as section universes makes no sense *)
       assert false
@@ -491,8 +491,8 @@ let name_instance inst =
         let qid = Nametab.shortest_qualid_of_universe na in
         Name (Libnames.qualid_basename qid)
       with Not_found ->
-        (** Best-effort naming from the string representation of the level.
-            See univNames.ml for a similar hack. *)
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
         Name (Id.of_string_soft (Univ.Level.to_string lvl))
   in
   Array.map map (Univ.Instance.to_array inst)
diff --git a/library/libnames.mli b/library/libnames.mli
index 9960603cbb..bbb4d2a058 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,8 +94,8 @@ val qualid_basename : qualid -> Id.t
 val default_library : DirPath.t
 
 (** This is the root of the standard library of Coq *)
-val coq_root : module_ident (** "Coq" *)
-val coq_string : string (** "Coq" *)
+val coq_root : module_ident (* "Coq" *)
+val coq_string : string (* "Coq" *)
 
 (** This is the default root prefix for developments which doesn't
    mention a root *)
diff --git a/library/library.mli b/library/library.mli
index d298a371b5..c016352808 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -19,8 +19,8 @@ open Libnames
   written at various dates.
 *)
 
-(** {6 ... } *)
-(** Require = load in the environment + open (if the optional boolean
+(** {6 ... }
+    Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
 
diff --git a/library/nametab.ml b/library/nametab.ml
index f0f643d9b5..95890b2edf 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -107,6 +107,7 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+
   (** Matches a prefix of [qualid], useful for completion *)
   val match_prefixes : qualid -> t -> elt list
 end
diff --git a/library/nametab.mli b/library/nametab.mli
index b7926cf515..fccb8fd918 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -171,7 +171,9 @@ val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
 val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
 val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
 val exists_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
diff --git a/library/summary.ml b/library/summary.ml
index 9b22945919..b68f1fb01b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -92,7 +92,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
   | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
   end;
-  (** We must be independent on the order of the map! *)
+  (* We must be independent on the order of the map! *)
   let ufz name decl =
     try decl.unfreeze_function String.Map.(find name summaries)
     with Not_found ->
diff --git a/library/summary.mli b/library/summary.mli
index 7d91a79188..64222761ba 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -19,9 +19,9 @@ type marshallable =
 (** Types of global Coq states. The ['a] type should be pure and marshallable by
     the standard OCaml marshalling function. *)
 type 'a summary_declaration = {
-  (** freeze_function [true] is for marshalling to disk. 
-   *  e.g. lazy must be forced *)
   freeze_function : marshallable -> 'a;
+  (** freeze_function [true] is for marshalling to disk.
+   *  e.g. lazy must be forced *)
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }