diff options
Diffstat (limited to 'plugins/ltac/profile_ltac.ml')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index a853576f2..747669852 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -411,8 +411,7 @@ let _ = Declaremods.append_end_library_hook do_print_results_at_close let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; |