From 6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Aug 2019 16:47:49 +0200
Subject: Make sure that all query commands return a notice (not an info)
 feedback

As documented in the feedback API.
---
 plugins/ssr/ssrvernac.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index f3f1d713e9..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -279,7 +279,7 @@ let interp_search_notation ?loc tag okey =
       Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
     end; ntn
   | [ntn] ->
-    Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+    Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
   | ntns' ->
     let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
     err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
@@ -297,7 +297,7 @@ let interp_search_notation ?loc tag okey =
     let rbody = glob_constr_of_notation_constr ?loc body in
     let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
     let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
-    Feedback.msg_info (hov 0 m) in
+    Feedback.msg_notice (hov 0 m) in
   if List.length !scs > 1 then
     let scs' = List.remove (=) sc !scs in
     let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
@@ -464,7 +464,7 @@ let interp_modloc mr =
 
 let ssrdisplaysearch gr env t =
   let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
-  Feedback.msg_info (hov 2 pr_res ++ fnl ())
+  Feedback.msg_notice (hov 2 pr_res ++ fnl ())
 
 }
 
@@ -559,7 +559,7 @@ END
 let print_view_hints env sigma kind l =
   let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
   let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
-  Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
+  Feedback.msg_notice  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 }
 
-- 
cgit v1.2.3