diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-11 02:36:50 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-11 18:18:27 -0500 |
| commit | f912708d039a0ea5d1af71b15585abcc5ac0e800 (patch) | |
| tree | 7d7ed2509951f344902b6be8605a4773a7092dde /plugins | |
| parent | 54a9d18913db05c29837f60b4d82935207ec483a (diff) | |
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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9ae8bfe65..5225420dc 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 = |