diff options
Diffstat (limited to 'lib')
| -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 4442f36867..99a99c5522 100644 --- a/lib/richPp.mli +++ b/lib/richPp.mli @@ -26,7 +26,7 @@ module Indexer (Annotation : sig type t end) : sig end -(** Each annotation of the semi-structures document refers to the +(** Each annotation of the semi-structured document refers to the substring it annotates. *) type 'annotation located = { annotation : 'annotation option; |