From 47eacb1be09e6c4e634d9555fe2938eff2622fe1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 3 Sep 2019 16:52:57 +0200
Subject: Locations for notation deprecation warnings

---
 interp/syntax_def.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 302bb6ece2..9dded8656c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -100,7 +100,7 @@ let warn_deprecated_syntactic_definition =
 let search_syntactic_definition ?loc kn =
   let syndef = KNmap.find kn !syntax_table in
   let def = out_pat syndef.syndef_pattern in
-  Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+  Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
   def
 
 let search_filtered_syntactic_definition ?loc filter kn =
@@ -108,5 +108,5 @@ let search_filtered_syntactic_definition ?loc filter kn =
   let def = out_pat syndef.syndef_pattern in
   let res = filter def in
   if Option.has_some res then
-    Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+    Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
   res
-- 
cgit v1.2.3