fixed same_file (#1141)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 20 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 4afb677d5..17965558c 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -77,26 +77,18 @@ let version () =
 
 let is_in_coq_lib dir = 
   prerr_endline ("Is it a coq theory ? : "^dir);
-  try
-    let stat = Unix.stat dir in
-      List.exists 
-	(fun s -> 
-	   try
-	     let fdir = Filename.concat 
-	       Coq_config.coqlib 
-	       (Filename.concat "theories" s) 
-	     in
-	       prerr_endline (" Comparing to: "^fdir);
-	       let fstat = Unix.stat fdir in 
-		 (fstat.Unix.st_dev = stat.Unix.st_dev) &&
-		   (fstat.Unix.st_ino = stat.Unix.st_ino) && 
-		   (prerr_endline " YES";true)
-	   with _ -> prerr_endline " No(because of a local exn)";false
-	)
-	Coq_config.theories_dirs
-  with _ -> prerr_endline " No(because of a global exn)";false
-
-let is_in_loadpath dir = Library.is_in_load_paths (System.physical_path_of_string dir)
+  let is_same_file = same_file dir in
+  List.exists 
+    (fun s -> 
+      let fdir =
+        Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in
+      prerr_endline (" Comparing to: "^fdir);
+      if is_same_file fdir then (prerr_endline " YES";true)
+      else (prerr_endline"NO";false))
+    Coq_config.theories_dirs
+
+let is_in_loadpath dir =
+  Library.is_in_load_paths (System.physical_path_of_string dir)
 
 let is_in_coq_path f = 
   try