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 /tactics/equality.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 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |