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


From f912708d039a0ea5d1af71b15585abcc5ac0e800 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 11 Dec 2017 02:36:50 -0500
Subject: Use msg_info for LtacProf

This way, `Time Show Ltac Profile` shows the profile in `*response*` in
PG, without an extra `infomsg` tag on the timing.
---
 plugins/ltac/profile_ltac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9ae8bfe65b..5225420dc4 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -408,7 +408,7 @@ let print_results_filter ~cutoff ~filter =
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~cutoff ~filter results)
+  Feedback.msg_info (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =
-- 
cgit v1.2.3