diff options
Diffstat (limited to 'ide/richpp.mli')
| -rw-r--r-- | ide/richpp.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/ide/richpp.mli b/ide/richpp.mli index 0ceeeefc2..0fe4315b7 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,9 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> - (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> - 'annotation located Xml_datatype.gxml +val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is |