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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

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
-- 
cgit v1.2.3