diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-15 20:48:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 22:35:10 +0200 |
| commit | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (patch) | |
| tree | 78c30edd51e65c8e7014ac360c5027da77ff20b2 /library/goptions.ml | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
[cleanup] Unify all calls to the error function.
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 9b4fc9985..a803771cb 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -71,7 +71,7 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - error "Sorry, this table name is already used." + user_err Pp.(str "Sorry, this table name is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) @@ -214,11 +214,11 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - error "Sorry, this option name is already used." + user_err Pp.(str "Sorry, this option name is already used.") with Not_found -> if String.List.mem_assoc (nickname key) !string_table || String.List.mem_assoc (nickname key) !ref_table - then error "Sorry, this option name is already used." + then user_err Pp.(str "Sorry, this option name is already used.") open Libobject @@ -307,7 +307,7 @@ let set_option_value locality check_and_cast key v = | Some (name, depr, (read,write,append)) -> write (get_locality locality) (check_and_cast v (read ())) -let bad_type_error () = error "Bad type of value for this option." +let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") let check_int_value v = function | IntValue _ -> IntValue v |