diff options
| author |  Jason Gross <jgross@mit.edu> | 2015-06-23 10:12:41 +0200 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:39 -0400 |
| commit | 9ff2c9d8d042c9989b6a8138c308398c49ae116f (patch) | |
| tree | ab6abf0403a4db27fef257393795111284da20ae /toplevel/usage.ml | |
| parent | 45748e4efae8630cc13b0199dfcc9803341e8cd8 (diff) | |
LtacProf for Coq trunk
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f855c096e..fa57d9d21 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ +\n -profileltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ |