aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/usage.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c2a1bac73..de0f73ff4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -549,7 +549,7 @@ let parse_args arglist =
else native_compiler := true
|"-notop" -> unset_toplevel_name ()
|"-output-context" -> output_context := true
- |"-profileltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true
+ |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true
|"-q" -> no_load_rc ()
|"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
|"-quick" -> Flags.compilation_mode := BuildVio
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index fa57d9d21..5359a288a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -77,7 +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 -profile-ltac 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\"\