From 46a17141e6a19fff9dfeb1ef18cbba054e34e3c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 18 Sep 2017 18:14:25 +0200
Subject: Reporting locations in error messages about notation formats.

---
 lib/loc.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/loc.ml')

diff --git a/lib/loc.ml b/lib/loc.ml
index 06da13d44..4a935a9d9 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -62,6 +62,8 @@ let merge_opt l1 l2 = match l1, l2 with
 
 let unloc loc = (loc.bp, loc.ep)
 
+let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp }
+
 (** Located type *)
 type 'a located = t option * 'a
 
-- 
cgit v1.2.3