aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/goptions.ml16
-rw-r--r--library/impargs.ml7
-rw-r--r--library/lib.ml11
-rw-r--r--library/libobject.ml5
-rw-r--r--library/library.ml29
6 files changed, 38 insertions, 32 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cc7c4d7f1..a82f5260b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -950,7 +950,7 @@ type 'modast module_params =
let debug_print_modtab _ =
let pr_seg = function
| [] -> str "[]"
- | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+ | l -> str "[." ++ int (List.length l) ++ str ".]"
in
let pr_modinfo mp (prefix,substobjs,keepobjs) s =
s ++ str (string_of_mp mp) ++ (spc ())
diff --git a/library/goptions.ml b/library/goptions.ml
index ef25fa590..4f50fbfbd 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -35,7 +35,7 @@ type option_state = {
let nickname table = String.concat " " table
let error_undeclared_key key =
- error ((nickname key)^": no table or option of this type")
+ errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
(****************************************************************************)
(* 1- Tables *)
@@ -301,7 +301,9 @@ let declare_string_option =
let set_option_value locality check_and_cast key v =
let (name, depr, (_,read,write,lwrite,gwrite)) =
try get_option key
- with Not_found -> error ("There is no option "^(nickname key)^".")
+ with Not_found ->
+ errorlabstrm "Goptions.set_option_value"
+ (str "There is no option " ++ str (nickname key) ++ str ".")
in
let write = match locality with
| None -> write
@@ -364,9 +366,9 @@ let print_option_value key =
let s = read () in
match s with
| BoolValue b ->
- msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
+ msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
| _ ->
- msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
+ msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
let get_tables () =
let tables = !value_tab in
@@ -383,7 +385,7 @@ let get_tables () =
let print_tables () =
let print_option key name value depr =
- let msg = str (" "^(nickname key)^": ") ++ msg_option_value (name, value) in
+ let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
@@ -401,10 +403,10 @@ let print_tables () =
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
- (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ())
+ (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ())
!string_table (mt ()) ++
List.fold_right
- (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ())
+ (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ())
!ref_table (mt ()) ++
fnl ()
diff --git a/library/impargs.ml b/library/impargs.ml
index 4b0e2e3d1..94f53219e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -10,6 +10,7 @@ open Errors
open Util
open Names
open Globnames
+open Nameops
open Term
open Reduction
open Declarations
@@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l =
List.iter (function
| ExplByName id,(b,fi,forced) ->
if not forced then
- error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
+ errorlabstrm ""
+ (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
| ExplByPos (i,_id),_t ->
if i<1 || i>List.length autoimps then
- error ("Bad implicit argument number: "^(string_of_int i)^".")
+ errorlabstrm ""
+ (str "Bad implicit argument number: " ++ int i ++ str ".")
else
errorlabstrm ""
(str "Cannot set implicit argument number " ++ int i ++
diff --git a/library/lib.ml b/library/lib.ml
index 9977b6665..81db547ef 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -75,7 +75,8 @@ let classify_segment seg =
| (_,ClosedModule _) :: stk -> clean acc stk
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
| (_,OpenedModule (ty,_,_,_)) :: _ ->
- error ("there are still opened " ^ module_kind ty ^"s")
+ errorlabstrm "Lib.classify_segment"
+ (str "there are still opened " ++ str (module_kind ty) ++ str "s")
| (_,FrozenState _) :: stk -> clean acc stk
in
clean ([],[],[]) (List.rev seg)
@@ -274,7 +275,7 @@ let start_modtype = start_mod true None
let error_still_opened string oname =
let id = basename (fst oname) in
errorlabstrm ""
- (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.")
+ (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
let end_mod is_type =
let oname,fs =
@@ -318,7 +319,8 @@ let end_compilation_checks dir =
try match snd (find_entry_p is_opening_node) with
| OpenedSection _ -> error "There are some open sections."
| OpenedModule (ty,_,_,_) ->
- error ("There are some open "^module_kind ty^"s.")
+ errorlabstrm "Lib.end_compilation_checks"
+ (str "There are some open " ++ str (module_kind ty) ++ str "s.")
| _ -> assert false
with Not_found -> ()
in
@@ -369,7 +371,8 @@ let find_opening_node id =
let oname,entry = find_entry_p is_opening_node in
let id' = basename (fst oname) in
if not (Names.Id.equal id id') then
- error ("Last block to end has name "^(Names.Id.to_string id')^".");
+ errorlabstrm "Lib.find_opening_node"
+ (str "Last block to end has name " ++ pr_id id' ++ str ".");
entry
with Not_found -> error "There is nothing to end."
diff --git a/library/libobject.ml b/library/libobject.ml
index 5f2a2127d..74930d76e 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,6 +7,7 @@
(************************************************************************)
open Libnames
+open Pp
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
@@ -33,15 +34,13 @@ type 'a object_declaration = {
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
-let yell s = Errors.anomaly (Pp.str s)
-
let default_object s = {
object_name = s;
cache_function = (fun _ -> ());
load_function = (fun _ _ -> ());
open_function = (fun _ _ -> ());
subst_function = (fun _ ->
- yell ("The object "^s^" does not know how to substitute!"));
+ Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
classify_function = (fun obj -> Keep obj);
discharge_function = (fun _ -> None);
rebuild_function = (fun x -> x)}
diff --git a/library/library.ml b/library/library.ml
index b4261309f..1ffa1a305 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -126,7 +126,8 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- error ("Unknown library " ^ (DirPath.to_string dir))
+ errorlabstrm "Library.find_library"
+ (str "Unknown library " ++ str (DirPath.to_string dir))
let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
@@ -378,10 +379,10 @@ let access_table what tables dp i =
let t =
try fetch_delayed f
with Faulty f ->
- error
- ("The file "^f^" (bound to " ^ dir_path ^
- ") is inaccessible or corrupted,\n" ^
- "cannot load some "^what^" in it.\n")
+ errorlabstrm "Library.access_table"
+ (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+ str ") is inaccessible or corrupted,\ncannot load some " ++
+ str what ++ str " in it.\n")
in
tables := LibraryMap.add dp (Fetched t) !tables;
t
@@ -462,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
let m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
errorlabstrm "load_physical_library"
- (str ("The file " ^ f ^ " contains library") ++ spc () ++
+ (str "The file " ++ str f ++ str " contains library" ++ spc () ++
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
@@ -475,9 +476,7 @@ and intern_library_deps libs dir m from =
and intern_mandatory_library caller from libs (dir,d) =
let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
- ".vo makes inconsistent assumptions over library " ^
- DirPath.to_string dir));
+ errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
libs
let rec_intern_library libs mref =
@@ -487,7 +486,7 @@ let rec_intern_library libs mref =
let check_library_short_name f dir = function
| Some id when not (Id.equal id (snd (split_dirpath dir))) ->
errorlabstrm "check_library_short_name"
- (str ("The file " ^ f ^ " contains library") ++ spc () ++
+ (str "The file " ++ str f ++ str " contains library" ++ spc () ++
pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
pr_id id)
| _ -> ()
@@ -613,7 +612,7 @@ let safe_locate_module (loc,qid) =
try Nametab.locate_module qid
with Not_found ->
user_err_loc
- (loc,"import_library", str (string_of_qualid qid ^ " is not a module"))
+ (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
let import_module export modl =
(* Optimization: libraries in a raw in the list are imported
@@ -638,7 +637,7 @@ let import_module export modl =
try Declaremods.import_module export mp; aux [] l
with Not_found ->
user_err_loc (loc,"import_library",
- str ((string_of_qualid dir)^" is not a module")))
+ str (string_of_qualid dir) ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
@@ -650,8 +649,8 @@ let check_coq_overwriting p id =
let is_empty = match l with [] -> true | _ -> false in
if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
errorlabstrm ""
- (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
- ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
+ (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+ str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
(* Verifies that a string starts by a letter and do not contain
others caracters than letters, digits, or `_` *)
@@ -795,7 +794,7 @@ let save_library_to ?todo dir f otab =
msg_error (str"Could not compile the library to native code. Skipping.")
with reraise ->
let reraise = Errors.push reraise in
- let () = msg_warning (str ("Removed file "^f')) in
+ let () = msg_warning (str "Removed file " ++ str f') in
let () = close_out ch in
let () = Sys.remove f' in
iraise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:06:23 +0000