diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 34 |
1 files changed, 18 insertions, 16 deletions
@@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: coq.ml 8912 2006-06-07 11:20:58Z notin $ *) open Vernac open Vernacexpr @@ -72,23 +72,25 @@ 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 + 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_in_coq_path f = try let base = Filename.chop_extension (Filename.basename f) in |