From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Dec 2015 22:35:09 +0100
Subject: Do not compose "str" and "to_string" whenever possible.

For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
---
 plugins/extraction/table.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9feaea8cdb..30486879ee 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
+	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
-- 
cgit v1.2.3