diff options
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 64fdf3724d..f407e2fd5b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -95,11 +95,6 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. *) -val msg_error : ?loc:Loc.t -> Pp.t -> unit -[@@ocaml.deprecated "msg_error is an internal function and should not be \ - used unless you know what you are doing. Use \ - [CErrors.user_err] instead."] - val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) |