diff options
| author | coqbot-app[bot] | 2021-02-22 11:45:00 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-22 11:45:00 +0000 |
| commit | 3d1e3d41ac124a02902614317e6318d6cf7a3c38 (patch) | |
| tree | cb2a0240c94f702e8a66e8b8780e9ea5dfe55589 /lib | |
| parent | 20b2dd4caea233a6516d9470619de9995bcdad96 (diff) | |
| parent | 6da4ec3e1d9e484d5cd95c116fc1c961acedf3f7 (diff) | |
Merge PR #13828: Fix doc comment in pp.mli
Reviewed-by: ejgallego
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 |