diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-28 16:32:42 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-29 10:47:00 +0200 |
| commit | e1df1b77f8c72636b6e347f41f6f38976c86e909 (patch) | |
| tree | fc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /lib/flags.ml | |
| parent | ed53e048fc5e4b995c1e0c42bf1ba1611c331cce (diff) | |
-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 13525165a..d29064c97 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -226,6 +226,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 0.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode |