aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-22 14:29:58 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-22 14:29:58 +0000
commit08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (patch)
tree9b47cee57c927b638d9cfdab49890f21ec05c8cf /config
parentc1159f736c8d8f5b95bc53af7614a63f2ab9a86b (diff)
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
Diffstat (limited to 'config')
-rw-r--r--config/coq_config.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index f16ffbe51..94d0b6c93 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -36,6 +36,7 @@ val cflags : string (* arguments passed to gcc *)
val best : string (* byte/opt *)
val arch : string (* architecture *)
+val arch_is_win32 : bool
val osdeplibs : string (* OS dependant link options for ocamlc *)
val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)