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 ++--
 lib/flags.mli | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'lib')

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
diff --git a/lib/flags.mli b/lib/flags.mli
index 756d3b8515..1f68a88f3a 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -128,8 +128,8 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(* Disabling native code compilation for conversion and normalization *)
-val no_native_compiler : bool ref
+(* Native code compilation for conversion and normalization *)
+val native_compiler : bool ref
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 val print_mod_uid : bool ref
-- 
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')

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


From 5f8dc36fb2d65699233b9ac9a3ff9f93701a01cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 May 2015 12:49:41 +0200
Subject: The -list-tag options now prints the corresponding COQ_COLORS value.

---
 lib/terminal.ml  | 7 +++++--
 lib/terminal.mli | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/terminal.ml b/lib/terminal.ml
index 0f6b23af36..58851ed274 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -117,7 +117,7 @@ let is_extended = function
 | `INDEX _ | `RGB _ -> true
 | _ -> false
 
-let eval st =
+let repr st =
   let fg = match st.fg_color with
   | None -> []
   | Some c ->
@@ -152,7 +152,10 @@ let eval st =
   | Some true -> [7]
   | Some false -> [27]
   in
-  let tags = fg @ bg @ bold @ italic @ underline @ negative in
+  fg @ bg @ bold @ italic @ underline @ negative
+
+let eval st =
+  let tags = repr st in
   let tags = List.map string_of_int tags in
   Printf.sprintf "\027[%sm" (String.concat ";" tags)
 
diff --git a/lib/terminal.mli b/lib/terminal.mli
index f308ede323..49172e3ce3 100644
--- a/lib/terminal.mli
+++ b/lib/terminal.mli
@@ -46,6 +46,9 @@ val make : ?fg_color:color -> ?bg_color:color ->
 val merge : style -> style -> style
 (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *)
 
+val repr : style -> int list
+(** Generate the ANSI code representing the given style. *)
+
 val eval : style -> string
 (** Generate an escape sequence from a style. *)
 
-- 
cgit v1.2.3