diff options
| author | Regis-Gianas | 2014-11-04 23:04:30 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 23:04:39 +0100 |
| commit | 3b9ab8c8f596a66bf38b672d7e8cf32db3b08577 (patch) | |
| tree | 93fc4a0cf688efcb07c508a647592f17b69a7e77 /lib | |
| parent | d1569f060a114b113ea9f326f1dec1c1e3f101dc (diff) | |
lib/richPp: Cosmetics.
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; |