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.mli | |
| 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.mli')
| -rw-r--r-- | lib/flags.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 8fe64d24f..839c252cb 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -149,6 +149,7 @@ val tactic_context_compat : bool ref context vs. appcontext) is set. *) val profile_ltac : bool ref +val profile_ltac_cutoff : float ref (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref |