diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
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 ()) } |