diff options
| author | Guillaume Melquiond | 2015-04-23 14:55:11 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-23 16:02:45 +0200 |
| commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
| tree | c595fc1fafd00a08cb91e53002610df867cf5eed /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 0d3a1c17e4..141ae145dd 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 |