Fix doc comment in pp.mli

1 files changed, 25 insertions, 24 deletions

diff --git a/lib/pp.mli b/lib/pp.mli
index 12f1ba9bb2..b3c2301d34 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -10,30 +10,31 @@
 
 (** Coq document type. *)
 
-(** Pretty printing guidelines ******************************************)
-(*                                                                      *)
-(* `Pp.t` is the main pretty printing document type                     *)
-(* in the Coq system. Documents are composed laying out boxes, and      *)
-(* users can add arbitrary tag metadata that backends are free          *)
-(* to interpret.                                                        *)
-(*                                                                      *)
-(* The datatype has a public view to allow serialization or advanced    *)
-(* uses, however regular users are _strongly_ warned against its use,   *)
-(* they should instead rely on the available functions below.           *)
-(*                                                                      *)
-(* Box order and number is indeed an important factor. Try to create    *)
-(* a proper amount of boxes. The `++` operator provides "efficient"     *)
-(* concatenation, but using the list constructors is usually preferred. *)
-(*                                                                      *)
-(* That is to say, this:                                                *)
-(*                                                                      *)
-(* `hov [str "Term"; hov (pr_term t); str "is defined"]`                *)
-(*                                                                      *)
-(* is preferred to:                                                     *)
-(*                                                                      *)
-(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")`            *)
-(*                                                                      *)
-(************************************************************************)
+(**
+{4 Pretty printing guidelines}
+
+[Pp.t] is the main pretty printing document type
+in the Coq system. Documents are composed laying out boxes, and
+users can add arbitrary tag metadata that backends are free
+to interpret.
+
+The datatype has a public view to allow serialization or advanced
+uses, however regular users are _strongly_ warned against its use,
+they should instead rely on the available functions below.
+
+Box order and number is indeed an important factor. Try to create
+a proper amount of boxes. The [++] operator provides "efficient"
+concatenation, but using the list constructors is usually preferred.
+
+That is to say, this:
+
+[hov [str "Term"; hov (pr_term t); str "is defined"]]
+
+is preferred to:
+
+[hov (str "Term" ++ hov (pr_term t) ++ str "is defined")]
+*)
+
 
 (* XXX: Improve and add attributes *)
 type pp_tag = string