From e1df1b77f8c72636b6e347f41f6f38976c86e909 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Sep 2016 16:32:42 +0200 Subject: -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. --- toplevel/coqtop.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'toplevel/coqtop.ml') 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 ()) -- cgit v1.2.3