diff options
| author | Regis-Gianas | 2014-11-04 23:05:21 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 23:05:21 +0100 |
| commit | 7cc2bda87604f06bc453fa04b03f7d51dc7a1cb0 (patch) | |
| tree | 9013e1605e7c92fc3e6f96f2de93a700b664b087 /lib | |
| parent | 3b9ab8c8f596a66bf38b672d7e8cf32db3b08577 (diff) | |
lib/Ppconstr: Cosmetics.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/richPp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/richPp.mli b/lib/richPp.mli index 99a99c5522..59d4c6af43 100644 --- a/lib/richPp.mli +++ b/lib/richPp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This module produces semi-structured pretty-printing. *) +(** This module offers semi-structured pretty-printing. *) (** A pretty printer module must use an instance of the following functor to index annotations. The index must be used as Format.tag |