diff options
| author | Gaëtan Gilbert | 2019-02-08 14:10:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 14:10:22 +0100 |
| commit | 95e723892c336808aad0926c675f3e0ac8ba7d99 (patch) | |
| tree | 939aec8d4659c02ab5c5f29c4f74b59f1d50ecd7 /lib/flags.ml | |
| parent | bb967f18247fc79c7158a89a1fe160a558910460 (diff) | |
Remove global output_native_objects flag.
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 3 |
1 files changed, 0 insertions, 3 deletions
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 |