From fd33e3875b872f8b83c350427a9809e68d7fe009 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 Jun 2018 21:04:27 +0200
Subject: Fixes #7636: location missing on deprecated compatibility notations.

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 45c0e9c42d..1691ff6d86 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -999,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args =
   match intern_extended_global_of_qualid qid with
   | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
-      let (ids,c) = Syntax_def.search_syntactic_definition sp in
+      let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments ?loc;
       let args1,args2 = List.chop nids args in
-- 
cgit v1.2.3