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.

---
 interp/ppextend.ml  | 2 +-
 interp/ppextend.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 3ebc9b71d2..ce19dd8a92 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -36,5 +36,5 @@ type unparsing =
   | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
-  | UnpBox of ppbox * unparsing list
+  | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 6ff5a42728..7b62a2074b 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -29,5 +29,5 @@ type unparsing =
   | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
-  | UnpBox of ppbox * unparsing list
+  | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
-- 
cgit v1.2.3