diff options
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 |