diff options
Diffstat (limited to 'lib/pp.mli')
-rw-r--r-- | lib/pp.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 7a191b01a..45834dade 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -13,6 +13,7 @@ (* `Pp.t` or `Pp.std_ppcmds` 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 againt its use, *) |