diff options
49 files changed, 258 insertions, 221 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 9a1007acb..0f7ed8df5 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -67,13 +67,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d with Errors.UserError _ -> if_verbose msg_warning - (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -221,7 +221,7 @@ let print_loc loc = else let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) @@ -232,7 +232,7 @@ let rec explain_exn = function | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() ) | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> @@ -241,14 +241,14 @@ let rec explain_exn = function hov 0 (str "Stack overflow") | Match_failure(filename,pos1,pos2) -> hov 1 (anomaly_string () ++ str "Match failure in file " ++ - str (guill filename) ++ str " at line " ++ int pos1 ++ + guill filename ++ str " at line " ++ int pos1 ++ str " character " ++ int pos2 ++ report ()) | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) | Failure s -> hov 0 (str "Failure: " ++ str s ++ report ()) | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> @@ -294,7 +294,7 @@ let rec explain_exn = function Format.printf "@\n====== universes ====@\n"; Pp.pp (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); - str("\nCantApplyBadType at argument " ^ string_of_int n) + str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -309,7 +309,7 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + (str "(file \"" ++ str s ++ str "\", line " ++ int b ++ str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) @@ -323,7 +323,7 @@ let parse_args argv = | "-coqlib" :: s :: rem -> if not (exists_dir s) then - fatal_error (str ("Directory '"^s^"' does not exist")) false; + fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 02504c920..5ac718e3b 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str ("cannot find "^s^ - " in module"^(if List.length dirs > 1 then "s " else " ")) ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> anomaly ~label:locstr - (str ("ambiguous name "^s^" can represent ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) let gen_constant_in_modules locstr dirs s = @@ -86,7 +86,8 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(DirPath.to_string dir)^" has to be required first.") + errorlabstrm "Coqlib.check_required_library" + (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/interp/notation.ml b/interp/notation.ml index 80db2cb39..555dfa804 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -91,7 +91,9 @@ let declare_scope scope = (* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map -let error_unknown_scope sc = error ("Scope "^sc^" is not declared.") +let error_unknown_scope sc = + errorlabstrm "Notation" + (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = try String.Map.find scope !scope_map @@ -186,14 +188,14 @@ let declare_delimiters scope key = | Some oldkey when String.equal oldkey key -> () | Some oldkey -> msg_warning - (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); + (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; try let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); + msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -202,7 +204,7 @@ let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> user_err_loc - (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^".")) + (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) @@ -317,8 +319,7 @@ let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> user_err_loc (loc,"prim_token_interpreter", - str ("Cannot interpret in "^sc^" without requiring first module " - ^(List.last d)^".")) + str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -373,10 +374,9 @@ let declare_notation_interpretation ntn scopt pat df = let () = if String.Map.mem ntn sc.notations then let which_scope = match scopt with - | None -> "" - | Some _ -> " in scope " ^ scope in - let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in - msg_warning (strbrk message) + | None -> mt () + | Some _ -> str " in scope " ++ str scope in + msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) in let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in let () = scope_map := String.Map.add scope sc !scope_map in @@ -452,7 +452,7 @@ let interp_notation loc ntn local_scopes = try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err_loc - (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) + (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -784,8 +784,8 @@ let pr_scope_classes sc = match l with | [] -> mt () | _ :: l -> - let opt_s = match l with [] -> "" | _ -> "es" in - hov 0 (str ("Bound to class" ^ opt_s) ++ + let opt_s = match l with [] -> mt () | _ -> str "es" in + hov 0 (str "Bound to class" ++ opt_s ++ spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() let pr_notation_info prglob ntn c = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9be7abcfe..d2709d5e3 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -99,7 +99,7 @@ let verbose_compat kn def = function | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r | _ -> str " is a compatibility notation" in - let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in + let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in act (pr_syndef kn ++ pp_def ++ since) | _ -> () diff --git a/lib/dyn.ml b/lib/dyn.ml index a5e8fb9c2..056b68731 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -7,6 +7,7 @@ (************************************************************************) open Errors +open Pp (* Dynamics, programmed with DANGER !!! *) @@ -23,7 +24,7 @@ let create (s : string) = let () = if Int.Map.mem hash !dyntab then let old = Int.Map.find hash !dyntab in - let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in + let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in anomaly ~label:"Dyn.create" msg in let () = dyntab := Int.Map.add hash s !dyntab in @@ -31,8 +32,7 @@ let create (s : string) = let outfun (nh, rv) = if Int.equal hash nh then Obj.magic rv else - let msg = (Pp.str ("dyn_out: expected " ^ s)) in - anomaly msg + anomaly (str "dyn_out: expected " ++ str s) in (infun, outfun) @@ -43,8 +43,7 @@ let has_tag (s, _) tag = let tag (s,_) = try Int.Map.find s !dyntab with Not_found -> - let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in - anomaly msg + anomaly (str "Unknown dynamic tag " ++ int s) let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 diff --git a/lib/errors.ml b/lib/errors.ml index 13f391647..999d99ee0 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -69,12 +69,12 @@ let rec print_gen bottom stk e = let where = function | None -> mt () | Some s -> - if !Flags.debug then str ("in "^s^":") ++ spc () else mt () + if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () let raw_anomaly e = match e with | Anomaly (s, pps) -> where s ++ pps ++ str "." - | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".") - | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".") + | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." + | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." let print_backtrace e = match Backtrace.get_backtrace e with | None -> mt () @@ -249,7 +249,7 @@ let escape_string s = else escape_at s (i-1) in escape_at s (String.length s - 1) -let qstring s = str ("\""^escape_string s^"\"") +let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring let quote s = h 0 (str "\"" ++ s ++ str "\"") diff --git a/lib/system.ml b/lib/system.ml index 73095f9cd..d1cdd8efc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -118,7 +118,8 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> error ("Can't open " ^ name) + with e when Errors.noncritical e -> + errorlabstrm "System.open" (str "Can't open " ++ str name) let try_remove filename = try Sys.remove filename @@ -126,7 +127,8 @@ let try_remove filename = msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.") +let error_corrupted file s = + errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -201,7 +203,8 @@ let extern_intern ?(warn=true) magic = let reraise = Errors.push reraise in let () = try_remove filename in iraise reraise - with Sys_error s -> error ("System error: " ^ s) + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) and intern_state paths name = try let _,filename = find_file_in_path ~warn paths name in @@ -210,7 +213,7 @@ let extern_intern ?(warn=true) magic = close_in channel; v with Sys_error s -> - error("System error: " ^ s) + errorlabstrm "System.intern_state" (str "System error: " ++ str s) in (extern_state,intern_state) 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 diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 84e4a5732..992f9c59a 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -58,7 +58,7 @@ END let error_bad_arity loc n = let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in - user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^").")) + user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").") (* Interpreting attributes *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 45e5aaf54..a2bbf97ae 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -604,7 +604,8 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f) + errorlabstrm "FunInd.build_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in @@ -636,10 +637,12 @@ let build_case_scheme fa = (* let id_to_constr id = *) (* Constrintern.global_reference id *) (* in *) - let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) - with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + let funs = + let (_,f,_) = fa in + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + with Not_found -> + errorlabstrm "FunInd.build_case_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 738ade8ca..1c409500e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,9 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Constrintern.locate_reference princ_ref - with Not_found -> Errors.error ("cannot find "^ Id.to_string id) + with Not_found -> + Errors.errorlabstrm "IndFun.const_of_id" + (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = match (Term.kind_of_term t) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0999b95d7..b9902a9fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,7 +305,8 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then error ("check_not_nested : failure "^Id.to_string x) + then errorlabstrm "Recdef.check_not_nested" + (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 01e1154e5..c2281e13a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context x (named_context env) then - error ("The variable "^(Id.to_string x)^" is already declared.") + errorlabstrm "Unification.make_abstraction_core" + (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else x in diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f8264e5af..a669aef9a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1260,13 +1260,12 @@ module Make and pr_tacarg = function | TacDynamic (loc,t) -> - pr_with_comments loc ( - str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>") - ) + pr_with_comments loc + (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>") | MetaIdArg (loc,true,s) -> - pr_with_comments loc (str ("$" ^ s)) + pr_with_comments loc (str "$" ++ str s) | MetaIdArg (loc,false,s) -> - pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s)) + pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s) | Reference r -> pr.pr_reference r | ConstrMayEval c -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89ffae4b3..c6b1b672f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1253,7 +1253,7 @@ module Make and pr_extend s cl = let pr_arg a = try pr_gen a - with Failure _ -> str ("<error in "^fst s^">") in + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in try let rl = Egramml.get_extend_vernac_rule s in let start,rl,cl = @@ -1271,7 +1271,7 @@ module Make (start,cl) rl in hov 1 pp with Not_found -> - hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") + hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") in pr_vernac diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 4a66c33df..e50435cda 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -180,16 +180,16 @@ let print_opacity ref = | None -> [] | Some s -> [pr_global ref ++ str " is " ++ - str (match s with - | FullyOpaque -> "opaque" + match s with + | FullyOpaque -> str "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> - "basically transparent but considered opaque for reduction" + str "basically transparent but considered opaque for reduction" | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> - "transparent" + str "transparent" | TransparentMaybeOpacified (Conv_oracle.Level n) -> - "transparent (with expansion weight "^string_of_int n^")" + str "transparent (with expansion weight " ++ int n ++ str ")" | TransparentMaybeOpacified Conv_oracle.Expand -> - "transparent (with minimal expansion weight)")] + str "transparent (with minimal expansion weight)"] (*******************) (* *) @@ -386,9 +386,9 @@ let print_located_qualid name flags ref = | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then - str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id + str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id else - str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> prlist_with_sep fnl (fun (o,oqid) -> diff --git a/printing/printer.ml b/printing/printer.ml index 0d3a1c17e..141ae145d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -654,7 +654,7 @@ let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in let g = Goal.get_by_uid id in let pr gs = - v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut () + v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () ++ pr_goal gs) in try @@ -723,7 +723,7 @@ let pr_assumptionset env s = try pr_constant env kn with Not_found -> let mp,_,lab = repr_con kn in - str (string_of_mp mp ^ "." ^ Label.to_string lab) + str (string_of_mp mp) ++ str "." ++ pr_label lab in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c8cb1d1cc..9b358210a 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -12,6 +12,7 @@ open Names open Evd open Evarutil open Evarsolve +open Pp (******************************************) (* Instantiation of existential variables *) @@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc - (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ - string_of_existential evk)) + (loc,"", str "Instance is not well-typed in the environment of " ++ + str (string_of_existential evk)) in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8206ca1b..898588d9e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - error ("Cannot create self-referring hypothesis "^Id.to_string x); + errorlabstrm "Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) = (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -522,7 +525,8 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ Id.to_string id ^ " is already declared."); + errorlabstrm "Logic.prim_refiner" + (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in @@ -550,11 +554,10 @@ let prim_refiner r sigma goal = | (f,n,ar)::oth -> let ((sp',_),u') = check_ind env n ar in if not (eq_mind sp sp') then - error ("Fixpoints should be on the same " ^ - "mutual inductive declaration."); + error "Fixpoints should be on the same mutual inductive declaration."; if !check && mem_named_context f (named_context_of_val sign) then - error - ("Name "^Id.to_string f^" already used in the environment"); + errorlabstrm "Logic.prim_refiner" + (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> Evd.Monad.List.map (fun (_,_,c) sigma -> @@ -584,8 +587,7 @@ let prim_refiner r sigma goal = try let _ = find_coinductive env sigma b in () with Not_found -> - error ("All methods must construct elements " ^ - "in coinductive types.") + error "All methods must construct elements in coinductive types." in let firsts,lasts = List.chop j others in let all = firsts@(f,cl)::lasts in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1383d7556..d25f7e915 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.declare_reduction" + (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then error ("Reference to undefined reduction expression "^s) + then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.decl_red_expr" + (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; red_expr_tab := String.Map.add s e !red_expr_tab @@ -232,7 +234,8 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - error("unknown user-defined reduction \""^s^"\""))) + errorlabstrm "Redexpr.reduction_of_red_expr" + (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3cc81daf5..d7f4b5ead 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -11,6 +11,7 @@ open Names open Pp open Tacexpr open Termops +open Nameops let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -231,17 +232,16 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function - | Anonymous -> " (unbound)" - | Name id -> " (bound to "^(Names.Id.to_string id)^")" + | Anonymous -> str " (unbound)" + | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ - str ((Names.Id.to_string id)^(hyp_bound ido)^ - " has been matched: ") ++ print_constr_env env c) + msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + str " has been matched: " ++ print_constr_env env c) else return () (* Prints the matched conclusion *) @@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ - " cannot match: ") ++ + msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ + str " cannot match: " ++ Hook.get prmatchpatt env sigma hyp) else return () diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 048bd637a..ad8164fa6 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -66,7 +66,7 @@ let find_base bas = try raw_find_base bas with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist.")) + (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = List.rev_map snd (HintDN.find_all (find_base bas)) diff --git a/tactics/equality.ml b/tactics/equality.ml index 816b54f02..5d6fcc5b1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl = let _ = Global.lookup_constant c1' in c1' with Not_found -> - let rwr_thm = Label.to_string l' in - error ("Cannot find rewrite principle "^rwr_thm^".") + errorlabstrm "Equality.find_elim" + (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") end | _ -> destConstRef pr1 end diff --git a/tactics/hints.ml b/tactics/hints.ml index 55d62e151..f83aa5601 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -598,7 +598,7 @@ let current_pure_db () = List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable)) let error_no_such_hint_database x = - error ("No such Hint database: "^x^".") + errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index ac8b4923e..60ce0e0dc 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -52,7 +52,7 @@ let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting")) + anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") let find_reference dir s = let gr = lazy (try_find_global_reference dir s) in diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 84c0a99b1..ffff44d5b 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -43,7 +43,7 @@ end module MLTacMap = Map.Make(MLName) let pr_tacname t = - t.mltac_plugin ^ "::" ^ t.mltac_tactic + str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic let tac_tab = ref MLTacMap.empty @@ -52,9 +52,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = if MLTacMap.mem s !tac_tab then if overwrite then let () = tac_tab := MLTacMap.remove s !tac_tab in - msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s)) + msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) else - Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ ".")) + Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in tac_tab := MLTacMap.add s t !tac_tab @@ -63,7 +63,7 @@ let interp_ml_tactic s = MLTacMap.find s !tac_tab with Not_found -> Errors.errorlabstrm "" - (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") + (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) (* Tactic registration *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0a746d283..7ce158fd1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1040,8 +1040,8 @@ let read_pattern lfun ist env sigma = function let cons_and_check_name id l = if Id.List.mem id l then user_err_loc (dloc,"read_match_goal_hyps", - strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^ - " used twice in the same pattern.")) + str "Hypothesis pattern-matching variable " ++ pr_id id ++ + str " used twice in the same pattern.") else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 17ac7a4b6..5ba53a764 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -615,7 +615,8 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") + errorlabstrm "Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b40c8d0e7..8117e4131 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -139,7 +139,8 @@ let introduction ?(check=true) id = let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if check && mem_named_context id hyps then - error ("Variable " ^ Id.to_string id ^ " is already declared.") + errorlabstrm "Tactics.introduction" + (str "Variable " ++ pr_id id ++ str " is already declared.") in match kind_of_term (whd_evar sigma concl) with | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b @@ -1870,8 +1871,8 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - error ("Not an inductive goal with "^ - string_of_int n ^ String.plural n " constructor"^".") + errorlabstrm "Tactics.check_number_of_constructors" + (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; if i > nconstr then error "Not enough constructors." @@ -3042,7 +3043,7 @@ let make_up_names n ind_opt cname = let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in - error ("Cannot recognize "^s^"an induction scheme.") + errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") let glob = Universes.constr_of_global diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 26ff7b92f..96bb89e2a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -19,6 +19,7 @@ open Termops open Declarations open Names open Globnames +open Nameops open Inductiveops open Tactics open Ind_tables @@ -338,7 +339,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) - else error ("Var "^(Id.to_string s)^" seems unknown.") + else errorlabstrm "AutoIndDecl.do_replace_lb" + (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) with e when Errors.noncritical e -> @@ -395,7 +397,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) - else error ("Var "^(Id.to_string s)^" seems unknown.") + else errorlabstrm "AutoIndDecl.do_replace_bl" + (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) with e when Errors.noncritical e -> @@ -502,8 +505,8 @@ let eqI ind l = (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff - with Not_found -> error - ("The boolean equality on "^(string_of_mind (fst ind))^" is needed."); + with Not_found -> errorlabstrm "AutoIndDecl.eqI" + (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index b29ba1efc..a0892bed9 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -20,7 +20,7 @@ let print_loc loc = let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" (** Invariant : exceptions embedded in EvaluatedError satisfy Errors.noncritical *) @@ -33,10 +33,10 @@ exception EvaluatedError of std_ppcmds * exn option let explain_exn_default = function (* Basic interaction exceptions *) - | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) - | Compat.Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) - | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg)) + | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") diff --git a/toplevel/command.ml b/toplevel/command.ml index 754ad8526..cdeecf1bb 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -609,8 +609,7 @@ let declare_mutual_inductive_with_eliminations mie impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error ("Records declared with the keywords Record or Structure cannot be recursive." ^ - "You can, however, define recursive records using the Inductive or CoInductive command.") + error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." else error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") | _ -> () @@ -697,19 +696,19 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - Id.to_string y^" depends on "^Id.to_string x^" but not conversely" + pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely" else if Id.List.mem y xge then - Id.to_string x^" depends on "^Id.to_string y^" but not conversely" + pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely" else - Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in - let e = if List.is_empty rest then reason else "e.g.: "^reason in + pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in + let e = if List.is_empty rest then reason else str "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix - then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + then str "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in - strbrk ("Not a fully mutually defined "^k) ++ fnl () ++ - strbrk ("("^e^").") ++ fnl () ++ w + str "Not a fully mutually defined " ++ str k ++ fnl () ++ + str "(" ++ e ++ str ")." ++ fnl () ++ w let check_mutuality env isfix fixl = let names = List.map fst fixl in diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index f1d8a4923..19d4363ab 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -134,6 +134,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); + msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); Flags.V8_2 - | s -> Errors.error ("Unknown compatibility version \""^s^"\".") + | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 52fa9e01e..caaf8054b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -176,7 +176,7 @@ let print_location_in_file {outer=s;inner=fname} loc = try let (line, bol) = line_of_pos 1 0 0 in hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ str", line " ++ int line ++ str", characters " ++ Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e9e86953b..2df7c69c8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -38,7 +38,7 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); + ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); pp_flush () let warning s = msg_warning (strbrk s) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 5429e6608..ac8ca3a11 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -872,11 +872,11 @@ let explain_not_match_error = function quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = - str "Signature components for label " ++ str (Label.to_string l) ++ + str "Signature components for label " ++ pr_label l ++ str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." let explain_label_already_declared l = - str ("The label "^Label.to_string l^" is already declared.") + str "The label " ++ pr_label l ++ str " is already declared." let explain_application_to_not_path _ = strbrk "A module cannot be applied to another module application or " ++ @@ -1170,18 +1170,18 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if Int.equal n 0 then "no "^s^"s" - else if Int.equal n 1 then "1 "^s - else (string_of_int n^" "^s^"s") + if Int.equal n 0 then str "no " ++ str s ++ str "s" + else if Int.equal n 1 then str "1 " ++ str s + else (int n ++ str " " ++ str s ++ str "s") let explain_wrong_numarg_constructor env cstr n = str "The constructor " ++ pr_constructor env cstr ++ str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++ - str ") expects " ++ str (decline_string n "argument") ++ str "." + str ") expects " ++ decline_string n "argument" ++ str "." let explain_wrong_numarg_inductive env ind n = str "The inductive type " ++ pr_inductive env ind ++ - str " expects " ++ str (decline_string n "argument") ++ str "." + str " expects " ++ decline_string n "argument" ++ str "." let explain_unused_clause env pats = (* Without localisation diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 138e5189a..0d39466ed 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -23,6 +23,7 @@ open Util open Declare open Entries open Decl_kinds +open Pp (**********************************************************************) (* Registering schemes in the environment *) @@ -87,7 +88,8 @@ let declare_scheme_object s aux f = try let _ = Hashtbl.find scheme_object_table key in (* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) - error ("Scheme object "^key^" already declared.") + errorlabstrm "IndTables.declare_scheme_object" + (str "Scheme object " ++ str key ++ str " already declared.") with Not_found -> Hashtbl.add scheme_object_table key (s,f); key diff --git a/toplevel/locality.ml b/toplevel/locality.ml index f711dad94..1145a20bb 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp + (** * Managing locality *) let local_of_bool = function @@ -16,7 +18,8 @@ let check_locality locality_flag = match locality_flag with | Some b -> let s = if b then "Local" else "Global" in - Errors.error ("This command does not support the \""^s^"\" prefix.") + Errors.errorlabstrm "Locality.check_locality" + (str "This command does not support the \"" ++ str s ++ str "\" prefix.") | None -> () (** Extracting the locality flag *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 639ec1e6e..f4fabc4d3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -387,7 +387,8 @@ let rec find_pattern nt xl = function | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, Terminal s :: _ | Terminal s :: _, _ -> - error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") + errorlabstrm "Metasyntax.find_pattern" + (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> error msg_expected_form_of_recursive_notation | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> @@ -448,7 +449,8 @@ let rec get_notation_vars = function let vars = get_notation_vars sl in if Id.equal id ldots_var then vars else if Id.List.mem id vars then - error ("Variable "^Id.to_string id^" occurs more than once.") + errorlabstrm "Metasyntax.get_notation_vars" + (str "Variable " ++ pr_id id ++ str " occurs more than once.") else id::vars | (Terminal _ | Break _) :: sl -> get_notation_vars sl @@ -461,8 +463,8 @@ let analyze_notation_tokens l = recvars, List.subtract Id.equal vars (List.map snd recvars), l let error_not_same_scope x y = - error ("Variables "^Id.to_string x^" and "^Id.to_string y^ - " must be in the same scope.") + errorlabstrm "Metasyntax.error_not_name_scope" + (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") (**********************************************************************) (* Build pretty-printing rules *) @@ -710,7 +712,7 @@ let is_not_small_constr = function let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> - Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword")); + Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); Lexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l @@ -719,7 +721,7 @@ let rec define_keywords_aux = function (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function | GramConstrTerminal(IDENT k)::l -> - Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword")); + Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); Lexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -804,7 +806,7 @@ let pr_level ntn (from,args) = let error_incompatible_level ntn oldprec prec = errorlabstrm "" - (str ("Notation "^ntn^" is already defined") ++ spc() ++ + (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") @@ -871,14 +873,16 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level."); + errorlabstrm "Metasyntax.interp_modifiers" + (str s ++ str " is already assigned to an entry or constr level."); interp assoc level ((id,typ)::etyps) format extra l | SetItemLevel ([],n) :: l -> interp assoc level etyps format extra l | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level."); + errorlabstrm "Metasyntax.interp_modifiers" + (str s ++ str " is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l) | SetLevel n :: l -> @@ -905,7 +909,8 @@ let check_infix_modifiers modifiers = let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with - | (x,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.") + | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types" + (pr_id x ++ str " is unbound in the notation.") | _ -> () let no_syntax_modifiers = function diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0b6fc48c4..a7fb7a58f 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path = let convert_string d = try Names.Id.of_string d with UserError _ -> - msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root ~implicit = @@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -321,13 +321,13 @@ let reset_loaded_modules () = loaded_modules := [] let if_verbose_load verb f name ?path fname = if not verb then f name ?path fname else - let info = "[Loading ML file "^fname^" ..." in + let info = str "[Loading ML file " ++ str fname ++ str " ..." in try let path = f name ?path fname in - msg_info (str (info^" done]")); + msg_info (info ++ str " done]"); path with reraise -> - msg_info (str (info^" failed]")); + msg_info (info ++ str " failed]"); raise reraise (** Load a module for the first time (i.e. dynlink it) @@ -340,7 +340,8 @@ let trigger_ml_object verb cache reinit ?path name = add_loaded_module name (known_module_path name); if cache then perform_cache_obj name end else if not has_dynlink then - error ("Dynamic link not supported (module "^name^")") + errorlabstrm "Mltop.trigger_ml_object" + (str "Dynamic link not supported (module " ++ str name ++ str ")") else begin let file = file_of_name (Option.default name path) in let path = diff --git a/toplevel/search.ml b/toplevel/search.ml index 59283edf9..9e67eef00 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -32,7 +32,7 @@ module SearchBlacklist = let key = ["Search";"Blacklist"] let title = "Current search blacklist : " let member_message s b = - str ("Search blacklist does "^(if b then "" else "not ")^"include "^s) + str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s let synchronous = true end) @@ -253,7 +253,8 @@ let interface_search flags = let regexp = try Str.regexp s with e when Errors.noncritical e -> - Errors.error ("Invalid regexp: " ^ s) + Errors.errorlabstrm "Search.interface_search" + (str "Invalid regexp: " ++ str s) in extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Type_Pattern s, b) :: l -> @@ -271,7 +272,8 @@ let interface_search flags = let id = try Nametab.full_name_module qid with Not_found -> - Errors.error ("Module " ^ path ^ " not found.") + Errors.errorlabstrm "Search.interface_search" + (str "Module " ++ str path ++ str " not found.") in extract_flags name tpe subtpe ((id, b) :: mods) blacklist l | (Include_Blacklist, b) :: l -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 176a6c333..b3694d0e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -208,7 +208,7 @@ let display_cmd_header loc com = let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str (" ["^cmd^"] ")); + str " [" ++ str cmd ++ str "] "); Pp.flush_all () let rec vernac_com verbosely checknav (loc,com) = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cfa9bddc6..f33c71d8a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -351,7 +351,7 @@ let dump_universes_gen g s = try Univ.dump_universes output_constraint g; close (); - msg_info (str ("Universes written to file \""^s^"\".")) + msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> let reraise = Errors.push reraise in close (); @@ -610,16 +610,14 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor declaration cannot be exported. " ^ - "Remove the \"Export\" and \"Import\" keywords from every functor " ^ - "argument.") + error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -641,7 +639,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Interactive Module "^ Id.to_string id ^" started")); + (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -651,9 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" and " ^ - "\"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -661,14 +657,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Module "^ Id.to_string id ^" is defined")); + (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -690,7 +686,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Interactive Module Type "^ Id.to_string id ^" started")); + (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -701,9 +697,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" " ^ - "and \"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_module_ast @@ -711,12 +705,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Module Type "^ Id.to_string id ^" is defined")) + (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref loc mp "modtype"; - if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined")) + if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -868,7 +862,8 @@ let vernac_set_used_variables e = let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then - error ("Unknown variable: " ^ Id.to_string id)) + errorlabstrm "vernac_set_used_variables" + (str "Unknown variable: " ++ pr_id id)) l; let closure_l = List.map pi1 (set_used_variables l) in let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in @@ -914,7 +909,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> msg_warning (str ("Cd failed: " ^ err)) + with Sys_error err -> msg_warning (str "Cd failed: " ++ str err) end; if_verbose msg_info (str (Sys.getcwd())) @@ -1051,15 +1046,16 @@ let vernac_declare_arguments locality r l nargs flags = let inf_names = let ty = Global.type_of_global_unsafe sr in Impargs.compute_implicits_names (Global.env ()) ty in - let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in let rec check li ld ls = match li, ld, ls with | [], [], [] -> () | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls | [], _::_, (Some _)::ls when extra_scope_flag -> error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".") - | l, [], _ -> error ("The following arguments are not declared: " ^ - (String.concat ", " (List.map string_of_name l)) ^ ".") + | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" + (str "Extra argument " ++ pr_name x ++ str ".") + | l, [], _ -> errorlabstrm "vernac_declare_arguments" + (str "The following arguments are not declared: " ++ + prlist_with_sep pr_comma pr_name l ++ str ".") | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with @@ -1087,9 +1083,6 @@ let vernac_declare_arguments locality r l nargs flags = let renamed_arg = ref None in let set_renamed a b = if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in - let pr_renamed_arg () = match !renamed_arg with None -> "" - | Some (o,n) -> - "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in @@ -1103,7 +1096,8 @@ let vernac_declare_arguments locality r l nargs flags = let sr', impl = List.fold_map (fun b -> function | (Anonymous, _,_, true, max), Name id -> assert false | (Name x, _,_, true, _), Anonymous -> - error ("Argument "^Id.to_string x^" cannot be declared implicit.") + errorlabstrm "vernac_declare_arguments" + (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> set_renamed iid id; b || not (Id.equal iid id), Some (ExplByName id, max, false) @@ -1116,8 +1110,12 @@ let vernac_declare_arguments locality r l nargs flags = some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error ("To rename arguments the \"rename\" flag must be specified." - ^ pr_renamed_arg ()) + errorlabstrm "vernac_declare_arguments" + (str "To rename arguments the \"rename\" flag must be specified." ++ + match !renamed_arg with + | None -> mt () + | Some (o,n) -> + str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".") else Arguments_renaming.rename_arguments (make_section_locality locality) sr names_decl; @@ -1581,7 +1579,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> Errors.error ("No such goal: "^string_of_int n^".")) + Failure _ -> errorlabstrm "print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let (id,bdyopt,typ) = Context.lookup_named id hyps in @@ -1674,8 +1673,8 @@ let interp_search_about_item env = (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - error ("Unable to interp \""^s^"\" either as a reference or \ - as an identifier component") + errorlabstrm "interp_search_about_item" + (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") let vernac_search s gopt r = let r = interp_search_restriction r in |