diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 14:55:11 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 16:02:45 +0200 |
| commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
| tree | c595fc1fafd00a08cb91e53002610df867cf5eed /interp/coqlib.ml | |
| parent | 915c8f15965fe8e7ee9d02a663fd890ef80539ad (diff) | |
Remove almost all the uses of string concatenation when building error messages.
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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 *) |