From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: Disable precompilation for native_compute by default.

Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.

Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.

If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.

Failure to precompile is a hard error, since it is now explicitly required
by the user.
---
 lib/flags.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index c8e7f7afed..f87dd5c2c8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -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
-- 
cgit v1.2.3


From 81eb133d64ac81cbf6962d624b20c1aa55c2baae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Apr 2015 11:16:05 +0200
Subject: Adding an option -w to control Coq warning output.

For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
---
 lib/flags.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index f87dd5c2c8..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
 
-- 
cgit v1.2.3