From 31ebb89fe48efe92786b1cddc3ba62e7dfc4e739 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 3 Sep 2004 15:05:54 +0000
Subject: Bug List.hd vs list_last

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6056 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 631f8f88cd..d220036379 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -68,7 +68,7 @@ let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
 let check_coq_overwriting p = 
-  if string_of_id (List.hd (repr_dirpath p)) = "Coq" then
+  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
     error "The \"Coq\" logical root directory is reserved for the Coq library"
 
 let set_include d p = push_include (d,p)
-- 
cgit v1.2.3