Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

4 files changed, 13 insertions, 7 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
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
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. *)