aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/profile_ltac_tactics.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 2b1106ee2..f09566063 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -13,7 +13,7 @@
open Profile_ltac
open Stdarg
-DECLARE PLUGIN "profile_ltac_plugin"
+DECLARE PLUGIN "ltac_plugin"
let tclSET_PROFILING b =
Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b))
@@ -22,7 +22,7 @@ TACTIC EXTEND start_ltac_profiling
| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
END
-TACTIC EXTEND stop_profiling
+TACTIC EXTEND stop_ltac_profiling
| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
END