diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 4 |
2 files changed, 4 insertions, 4 deletions
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 |