diff options
author | 2016-09-28 16:32:42 +0200 | |
---|---|---|
committer | 2016-09-29 10:47:00 +0200 | |
commit | e1df1b77f8c72636b6e347f41f6f38976c86e909 (patch) | |
tree | fc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /toplevel | |
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 'toplevel')
-rw-r--r-- | toplevel/coqtop.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ee331e37c..47d433d79 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -523,6 +523,7 @@ let parse_args arglist = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) |"-require" -> add_require (next ()) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |