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