aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-28 16:32:42 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-29 10:47:00 +0200
commite1df1b77f8c72636b6e347f41f6f38976c86e909 (patch)
treefc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /toplevel
parented53e048fc5e4b995c1e0c42bf1ba1611c331cce (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.ml1
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 ())