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.
---
 interp/coqlib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5ac718e3b0..b309f26cd6 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -87,7 +87,7 @@ let check_required_library d =
 *)
 (* or failing ...*)
       errorlabstrm "Coqlib.check_required_library"
-        (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+        (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
-- 
cgit v1.2.3