diff options
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index d2877edc5..5f8b2f736 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -20,6 +20,6 @@ include Ppconstrsig.Pp Please refer to {!RichPp} to know what are the requirements over [Indexer.index] behavior. *) -module RichPp (Indexer : sig val index : Ppannotation.t -> string end) +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) : Ppconstrsig.Pp |