diff options
Diffstat (limited to 'toplevel/vernacinterp.ml')
| -rw-r--r-- | toplevel/vernacinterp.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 7fbd2b11..d81e3d6b 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -8,7 +8,7 @@ open Util open Pp -open Errors +open CErrors type deprecation = bool type vernac_command = Genarg.raw_generic_argument list -> unit -> unit @@ -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 - msg_warning (str "Deprecated vernacular command: " ++ pr) + warn_deprecated_command pr; in loc:= "Checking arguments"; let hunk = callback converted_args in @@ -66,7 +71,7 @@ let call ?locality (opn,converted_args) = with | Drop -> raise Drop | reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in if !Flags.debug then - msg_debug (str"Vernac Interpreter " ++ str !loc); + Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc); iraise reraise |