From 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 Aug 2013 14:29:58 +0000 Subject: Misc changes around coqtop.ml : - Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/nativelib.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 6b2b4aa7c..c9da5222f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -32,13 +32,12 @@ let open_header = List.map mk_open open_header let compiler_name = Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ()) -let ( / ) a b = Filename.concat a b +let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) -let include_dirs () = [Filename.temp_dir_name; - coqlib ~fail:Errors.error / "kernel"; - coqlib ~fail:Errors.error / "library"] +let include_dirs () = + [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) -- cgit v1.2.3