diff options
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 *) |