diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 32 |
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 |