From c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Jun 2016 00:41:33 +0200 Subject: [feedback] Add optional ?loc parameter to loggers. This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished. --- interp/syntax_def.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/syntax_def.ml') 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 -- cgit v1.2.3