aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml6
-rw-r--r--library/goptions.ml8
-rw-r--r--library/impargs.ml4
-rw-r--r--library/lib.ml24
-rw-r--r--library/libnames.ml4
-rw-r--r--library/library.ml2
-rw-r--r--library/nametab.ml4
7 files changed, 26 insertions, 26 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3a263b1e1..08c33b5c1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -345,7 +345,7 @@ let get_applications mexpr =
let rec get params = function
| MEident mp -> mp, params
| MEapply (fexpr, mp) -> get (mp::params) fexpr
- | MEwith _ -> error "Non-atomic functor application."
+ | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
in get [] mexpr
(** Create the substitution corresponding to some functor applications *)
@@ -353,7 +353,7 @@ let get_applications mexpr =
let rec compute_subst env mbids sign mp_l inl =
match mbids,mp_l with
| _,[] -> mbids,empty_subst
- | [],r -> error "Application of a functor with too few arguments."
+ | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
| mbid::mbids,mp::mp_l ->
let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
let mb = Environ.lookup_module mp env in
@@ -777,7 +777,7 @@ let rec decompose_functor mpl typ =
match mpl, typ with
| [], _ -> typ
| _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
- | _ -> error "Application of a functor with too much arguments."
+ | _ -> user_err Pp.(str "Application of a functor with too much arguments.")
exception NoIncludeSelf
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
diff --git a/library/impargs.ml b/library/impargs.ml
index a63264b66..885185da1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -364,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l =
with Not_found -> l, None
in
if not (List.distinct l) then
- error ("Some parameters are referred more than once.");
+ user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k l = function
| (Name id,imp)::imps ->
@@ -658,7 +658,7 @@ let check_inclusion l =
let rec aux = function
| n1::(n2::_ as nl) ->
if n1 <= n2 then
- error "Sequences of implicit arguments must be of different lengths.";
+ user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
aux nl
| _ -> () in
aux (List.map (fun (imps,_) -> List.length imps) l)
diff --git a/library/lib.ml b/library/lib.ml
index ddd2ed6af..4ad4e261d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -76,7 +76,7 @@ let classify_segment seg =
(* LEM; TODO: Understand what this does and see if what I do is the
correct thing for ClosedMod(ule|type) *)
| (_,ClosedModule _) :: stk -> clean acc stk
- | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
| (_,OpenedModule (ty,_,_,_)) :: _ ->
user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
@@ -184,7 +184,7 @@ let split_lib_gen test =
| [] -> None
in
match findeq [] !lib_state.lib_stk with
- | None -> error "no such entry"
+ | None -> user_err Pp.(str "no such entry")
| Some r -> r
let eq_object_name (fp1, kn1) (fp2, kn2) =
@@ -222,7 +222,7 @@ let add_anonymous_entry node =
let add_leaf id obj =
if Names.ModPath.equal (current_mp ()) Names.initial_path then
- error ("No session module started (use -top dir)");
+ user_err Pp.(str "No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
add_entry oname (Leaf obj);
@@ -272,8 +272,8 @@ let current_mod_id () =
try match find_entry_p is_opening_node_or_lib with
| oname,OpenedModule (_,_,_,fs) -> basename (fst oname)
| oname,CompilingLibrary _ -> basename (fst oname)
- | _ -> error "you are not in a module"
- with Not_found -> error "no opened modules"
+ | _ -> user_err Pp.(str "you are not in a module")
+ with Not_found -> user_err Pp.(str "no opened modules")
let start_mod is_type export id mp fs =
@@ -305,7 +305,7 @@ let end_mod is_type =
else error_still_opened (module_kind ty) oname
| oname,OpenedSection _ -> error_still_opened "section" oname
| _ -> assert false
- with Not_found -> error "No opened modules."
+ with Not_found -> user_err (Pp.str "No opened modules.")
in
let (after,mark,before) = split_lib_at_opening oname in
lib_state := { !lib_state with lib_stk = before };
@@ -326,9 +326,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
(* TODO: use check_for_module ? *)
let start_compilation s mp =
if !lib_state.comp_name != None then
- error "compilation unit is already started";
+ user_err Pp.(str "compilation unit is already started");
if not (Names.DirPath.is_empty (current_sections ())) then
- error "some sections are already opened";
+ user_err Pp.(str "some sections are already opened");
let prefix = s, (mp, Names.DirPath.empty) in
let () = add_anonymous_entry (CompilingLibrary prefix) in
lib_state := { !lib_state with comp_name = Some s;
@@ -337,7 +337,7 @@ let start_compilation s mp =
let end_compilation_checks dir =
let _ =
try match snd (find_entry_p is_opening_node) with
- | OpenedSection _ -> error "There are some open sections."
+ | OpenedSection _ -> user_err Pp.(str "There are some open sections.")
| OpenedModule (ty,_,_,_) ->
user_err ~hdr:"Lib.end_compilation_checks"
(str "There are some open " ++ str (module_kind ty) ++ str "s.")
@@ -394,7 +394,7 @@ let find_opening_node id =
user_err ~hdr:"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."
+ with Not_found -> user_err Pp.(str "There is nothing to end.")
(* Discharge tables *)
@@ -428,7 +428,7 @@ let add_section () =
let check_same_poly p vars =
let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
if List.exists pred vars then
- error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+ user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
let add_section_variable id impl poly ctx =
match !sectab with
@@ -555,7 +555,7 @@ let close_section () =
| oname,OpenedSection (_,fs) -> oname,fs
| _ -> assert false
with Not_found ->
- error "No opened section."
+ user_err Pp.(str "No opened section.")
in
let (secdecls,mark,before) = split_lib_at_opening oname in
lib_state := { !lib_state with lib_stk = before };
diff --git a/library/libnames.ml b/library/libnames.ml
index dd74e192f..50f28b020 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
+ if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path.");
if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
- if Int.equal pos n then error (s ^ " is an invalid path.");
+ if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
in
diff --git a/library/library.ml b/library/library.ml
index 2b3381fa7..5a5f99cc5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab =
if !Flags.native_compiler then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
- error "Could not compile the library to native code."
+ user_err Pp.(str "Could not compile the library to native code.")
with reraise ->
let reraise = CErrors.push reraise in
let () = Feedback.msg_warning (str "Removed file " ++ str f') in
diff --git a/library/nametab.ml b/library/nametab.ml
index 1027e291c..2e4e98013 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -143,8 +143,8 @@ struct
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
- error ("Cannot mask the absolute name \""
- ^ U.to_string uname' ^ "\"!")
+ user_err Pp.(str @@ "Cannot mask the absolute name \""
+ ^ U.to_string uname' ^ "\"!")
| Nothing
| Relative _ -> mktree (Absolute (uname,o)) tree.map
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 00:09:43 +0000