diff options
Diffstat (limited to 'lib/loc.mli')
| -rw-r--r-- | lib/loc.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/loc.mli b/lib/loc.mli index d4061e044..fde490cc8 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -40,6 +40,11 @@ val merge : t -> t -> t val merge_opt : t option -> t option -> t option (** Merge locations, usually generating the largest possible span *) +val shift_loc : int -> int -> t -> t +(** [shift_loc loc n p] shifts the beginning of location by [n] and + the end by [p]; it is assumed that the shifts do not change the + lines at which the location starts and ends *) + (** {5 Located exceptions} *) val add_loc : Exninfo.info -> t -> Exninfo.info |