aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-12-11 02:13:59 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-12-11 18:18:27 -0500
commit54a9d18913db05c29837f60b4d82935207ec483a (patch)
treeaa7984996d66d223a036f5511526ac3d91a9841f /plugins
parent0275b5802ffd416dd0ed739955445a1c3c0287e9 (diff)
Allow LtacProf tactics to be called
This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
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