diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /ide/coq.ml | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
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 |