diff options
| author | Hugo Herbelin | 2015-05-15 11:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-15 11:39:49 +0200 |
| commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
| tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /lib/flags.ml | |
| parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index c8e7f7afed..313da0c5bd 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -160,7 +160,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,8 +206,8 @@ 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 |