diff options
Diffstat (limited to 'toplevel/vernacinterp.ml')
| -rw-r--r-- | toplevel/vernacinterp.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 1116a3104..0abc9e76d 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -42,6 +42,11 @@ let vinterp_map s = let vinterp_init () = Hashtbl.clear vernac_tab +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + (* Interpretation of a vernac command *) let call ?locality (opn,converted_args) = @@ -55,7 +60,7 @@ let call ?locality (opn,converted_args) = | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in - Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr) + warn_deprecated_command pr; in loc:= "Checking arguments"; let hunk = callback converted_args in |