From 8c684847844b25bd4ce071867fb480c9caa8cb62 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 22 Dec 2015 22:36:27 +0100
Subject: Avoid a pointless conversion/copy.

---
 library/library.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index ef621e16b..7aaa8b2e6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -602,7 +602,7 @@ let import_module export modl =
 let check_coq_overwriting p id =
   let l = DirPath.repr p in
   let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
+  if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
     errorlabstrm ""
       (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
-- 
cgit v1.2.3