diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/envars.ml | 29 | ||||
-rw-r--r-- | lib/envars.mli | 11 | ||||
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 1 |
4 files changed, 17 insertions, 26 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 8ebf84057..9b66c1f71 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -155,23 +155,21 @@ let exe s = s ^ Coq_config.exec_extension let ocamlfind () = Coq_config.ocamlfind -(** {2 Camlp4 paths} *) +(** {2 Camlp5 paths} *) -let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) +let guess_camlp5bin () = which (user_path ()) (exe "camlp5") -let camlp4bin () = - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () +let camlp5bin () = + if !Flags.boot then Coq_config.camlp5bin else + try guess_camlp5bin () with Not_found -> - Coq_config.camlp4bin + Coq_config.camlp5bin -let camlp4 () = camlp4bin () / exe Coq_config.camlp4 - -let camlp4lib () = +let camlp5lib () = if !Flags.boot then - Coq_config.camlp4lib + Coq_config.camlp5lib else - let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in + let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" @@ -206,11 +204,10 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4; - fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o; - fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); - fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); - fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; + fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ()); + fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ()); + fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/lib/envars.mli b/lib/envars.mli index 09f2b4ca1..1ccd1feff 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -56,14 +56,11 @@ val coqpath : string list (** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string -(** [camlp4bin ()] is the path to the camlp4 binary. *) -val camlp4bin : unit -> string +(** [camlp5bin ()] is the path to the camlp5 binary. *) +val camlp5bin : unit -> string -(** [camlp4lib ()] is the path to the camlp4 library. *) -val camlp4lib : unit -> string - -(** [camlp4 ()] is the camlp4 utility. *) -val camlp4 : unit -> string +(** [camlp5lib ()] is the path to the camlp5 library. *) +val camlp5lib : unit -> string (** Coq tries to honor the XDG Base Directory Specification to access the user's configuration files. diff --git a/lib/flags.ml b/lib/flags.ml index 01361dad5..415e4399a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -56,10 +56,8 @@ let in_toplevel = ref false let profile = false let ide_slave = ref false -let ideslave_coqtop_flags = ref None let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 33d281798..c82410f07 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -33,7 +33,6 @@ val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref -val ideslave_coqtop_flags : string option ref (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref |