From e4d5bbeecb4c5a4eca82700ba3946d9fd174e215 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 00:12:44 +0200 Subject: Moving back Ltac profiling to the Ltac folder. --- toplevel/coqtop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') 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 -- cgit v1.2.3