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

4 files changed, 11 insertions, 9 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f9f4d7f7f8..8f7e4470f9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -427,7 +427,7 @@ let locate_modtype qid =
   let all = Nametab.locate_extended_all_modtype qid in
   let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in
   let modtypes = List.map map all in
-  (** Don't forget the opened module types: they are not part of the same name tab. *)
+  (* Don't forget the opened module types: they are not part of the same name tab. *)
   let all = Nametab.locate_extended_all_dir qid in
   let map dir = let open Nametab.GlobDirRef in match dir with
   | DirOpenModtype _ -> Some (Dir dir, qid)
diff --git a/printing/printer.ml b/printing/printer.ml
index 2bbda279bd..83f1f8d8e9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -605,12 +605,12 @@ let print_evar_constraints gl sigma =
     let t1 = Evarutil.nf_evar sigma t1
     and t2 = Evarutil.nf_evar sigma t2 in
     let env =
-      (** We currently allow evar instances to refer to anonymous de Bruijn
-          indices, so we protect the error printing code in this case by giving
-          names to every de Bruijn variable in the rel_context of the conversion
-          problem. MS: we should rather stop depending on anonymous variables, they
-          can be used to indicate independency. Also, this depends on a strategy for 
-          naming/renaming *)
+      (* We currently allow evar instances to refer to anonymous de Bruijn
+         indices, so we protect the error printing code in this case by giving
+         names to every de Bruijn variable in the rel_context of the conversion
+         problem. MS: we should rather stop depending on anonymous variables, they
+         can be used to indicate independency. Also, this depends on a strategy for
+         naming/renaming *)
       Namegen.make_all_name_different env sigma in
     str" " ++
       hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
@@ -686,7 +686,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     | None -> GoalMap.empty
   in
 
-  (** Printing functions for the extra informations. *)
+  (* Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
@@ -753,7 +753,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     | None -> ()
   in
 
-  (** Main function *)
+  (* Main function *)
   match goals with
   | [] ->
       begin
diff --git a/printing/printer.mli b/printing/printer.mli
index b0232ec4ac..357f30d1f4 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -112,6 +112,7 @@ val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
 
 
 (** Contexts *)
+
 (** Display compact contexts of goals (simple hyps on the same line) *)
 val set_compact_context : bool -> unit
 val get_compact_context : unit -> bool
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ce9ee5ae6f..1ebde3d572 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -12,6 +12,7 @@
 
 (** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
 val write_diffs_option : string -> unit
+
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool