From 95e723892c336808aad0926c675f3e0ac8ba7d99 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 14:10:22 +0100
Subject: Remove global output_native_objects flag.

---
 lib/flags.ml  | 3 ---
 lib/flags.mli | 3 ---
 2 files changed, 6 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 29406ef275..7b1da2ff0e 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -118,8 +118,5 @@ let inline_level = ref default_inline_level
 let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
-(* Native code compilation for conversion and normalization *)
-let output_native_objects = ref false
-
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
diff --git a/lib/flags.mli b/lib/flags.mli
index b9c5e20f47..df9f464a14 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -112,9 +112,6 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(** When producing vo objects, also compile the native-code version *)
-val output_native_objects : bool ref
-
 (** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
-- 
cgit v1.2.3