diff options
| author | Maxime Dénès | 2017-06-14 18:12:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 18:12:03 +0200 |
| commit | 42843f73e30eae57684269479193389242a0c1b1 (patch) | |
| tree | 8a09a3452cd4d4afe91dd31cecd7899256bd0dfc /lib | |
| parent | e9ad450304fca010812a04e8417b111f4910156a (diff) | |
| parent | b5e90d92fc52e568f1ed6e65a4b611bdab80e8f5 (diff) | |
Merge PR#739: completing a sentence in a comment
Diffstat (limited to 'lib')
| -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 7a191b01a8..45834dade5 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, *) |