From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- ide/coq.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index 31c2f792..0b83b3c9 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -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 -- cgit v1.2.3