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 /toplevel/coqinit.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 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 "\".") |