diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /lib/flags.ml | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index c8e7f7af..ab4ac03f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -48,6 +48,8 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let test_mode = ref false + type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff type cache = Force @@ -160,7 +162,7 @@ let make_polymorphic_flag b = let program_mode = ref false let is_program_mode () = !program_mode -let warn = ref true +let warn = ref false let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x @@ -206,10 +208,14 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Disabling native code compilation for conversion and normalization *) -let no_native_compiler = ref Coq_config.no_native_compiler +(* Native code compilation for conversion and normalization *) +let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false let tactic_context_compat = ref false + +let dump_bytecode = ref false +let set_dump_bytecode = (:=) dump_bytecode +let get_dump_bytecode () = !dump_bytecode |