diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 15:16:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 18:35:08 +0200 |
| commit | d4725f692a5f202ca4c5d6341b586b0e377f6973 (patch) | |
| tree | 9cd74c65a51ca06547e9117b4d4901ec18a9519b /interp | |
| parent | 403c12ac3e8a9c3719aacbfa113600abc74846b7 (diff) | |
| parent | a10e3e0252560992128f490dfcb3d76c4bbf317b (diff) | |
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Was PR#223: Allow feedback messages to carry a location.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/syntax_def.ml | 2 |
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 |