diff options
| author | Regis-Gianas | 2014-11-04 23:05:50 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 23:05:50 +0100 |
| commit | f6a3e5523e49f7212ea6ddf7a38b477dae616d1a (patch) | |
| tree | 06e28e7e99863c054aae666ad0d69cf67dc538ac /lib | |
| parent | 7cc2bda87604f06bc453fa04b03f7d51dc7a1cb0 (diff) | |
lib/Ppconstr: Cosmetics.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/richPp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/richPp.mli b/lib/richPp.mli index 59d4c6af43..834115d40b 100644 --- a/lib/richPp.mli +++ b/lib/richPp.mli @@ -9,8 +9,8 @@ (** 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 - during the pretty-printing. *) + functor to index annotations. The index is to be used as a + [Format.tag] during the pretty-printing. *) (** The indices are Format.tags. *) type index = Format.tag (* = string *) |