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/notation.ml   | 2 +-
 interp/syntax_def.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/interp/notation.ml b/interp/notation.ml
index a78bc60e83..ea2173860d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1205,7 +1205,7 @@ let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try
     let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
-    Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+    Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
     n.not_interp, (n.not_location, sc)
   with Not_found ->
     user_err ?loc
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