diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.mli | 49 |
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 |