diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declaremods.ml | 6 | ||||
-rw-r--r-- | library/goptions.ml | 8 | ||||
-rw-r--r-- | library/impargs.ml | 4 | ||||
-rw-r--r-- | library/lib.ml | 24 | ||||
-rw-r--r-- | library/libnames.ml | 4 | ||||
-rw-r--r-- | library/library.ml | 2 | ||||
-rw-r--r-- | library/nametab.ml | 4 |
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 |