From 54a9d18913db05c29837f60b4d82935207ec483a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 11 Dec 2017 02:13:59 -0500
Subject: Allow LtacProf tactics to be called

This fixes #6378.  Previously the ML module was never declared anywhere.

Thanks to @cmangin for the pointer.
---
 plugins/ltac/profile_ltac_tactics.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 2b1106ee21..f095660638 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
 
-- 
cgit v1.2.3