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