From 46a17141e6a19fff9dfeb1ef18cbba054e34e3c3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Sep 2017 18:14:25 +0200 Subject: Reporting locations in error messages about notation formats. --- lib/loc.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'lib/loc.mli') 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 -- cgit v1.2.3