summaryrefslogtreecommitdiff
path: root/tools/coqdoc/cdglobals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/cdglobals.ml')
-rw-r--r--tools/coqdoc/cdglobals.ml22
1 files changed, 13 insertions, 9 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 443edc0b..de7290a4 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
let out_channel = ref stdout
+let ( / ) = Filename.concat
+
let coqdoc_out f =
if !output_dir <> "" && Filename.is_relative f then
if not (Sys.file_exists !output_dir) then
(Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
else
- Filename.concat !output_dir f
+ !output_dir / f
else
f
@@ -71,17 +73,19 @@ let normalize_filename f =
(** A weaker analog of the function in Envars *)
let guess_coqlib () =
- let file = "states/initial.coq" in
+ let file = "theories/Init/Prelude.vo" in
match Coq_config.coqlib with
- | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
- coqlib
+ | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
| Some _ | None ->
let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
- let rpath = if Coq_config.local then [] else
- (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
- let coqlib = List.fold_left Filename.concat prefix rpath in
- if Sys.file_exists (Filename.concat coqlib file) then coqlib
+ let rpath =
+ if Coq_config.local then []
+ else if Coq_config.arch_is_win32 then ["lib"]
+ else ["lib/coq"]
+ in
+ let coqlib = List.fold_left (/) prefix rpath in
+ if Sys.file_exists (coqlib / file) then coqlib
else prefix
let header_trailer = ref true