From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/vernacinterp.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'toplevel/vernacinterp.ml') 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 -- cgit v1.2.3