diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-14 00:12:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-14 00:28:42 +0200 |
| commit | e4d5bbeecb4c5a4eca82700ba3946d9fd174e215 (patch) | |
| tree | e2c0ff3071c4638fe5f16bdb36e79d28508dc82f /toplevel | |
| parent | 236627cdf081e51fce3bc54fdee4e40d4f6ca85e (diff) | |
Moving back Ltac profiling to the Ltac folder.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index de0f73ff4..aab20650a 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 - |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |