diff options
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 62b909516f..64fdf3724d 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Xml_datatype @@ -94,8 +96,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit consequences. *) val msg_error : ?loc:Loc.t -> Pp.t -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) +[@@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 *) |