aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/syntax_def.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 891b64fa1..9a1483b10 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -93,7 +93,7 @@ let is_verbose_compat () =
let verbose_compat kn def = function
| Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
let act =
- if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm ""
+ if !verbose_compat_notations then Feedback.msg_warning ?loc:None else errorlabstrm ""
in
let pp_def = match def with
| [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r