diff options
| author | Matej Košík | 2017-06-07 15:44:41 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-06-07 15:46:05 +0200 |
| commit | b5e90d92fc52e568f1ed6e65a4b611bdab80e8f5 (patch) | |
| tree | 27da240ea2a62d776e42ae320169ce32cb0952c3 /lib | |
| parent | 73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (diff) | |
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, *) |