Make sure that all query commands return a notice (not an info) feedback

As documented in the feedback API.

7 files changed, 32 insertions, 37 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3ed843649e..b5be1cdd89 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms =
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
-            let open Glob_term in
-            let env = Proofview.Goal.env gl in
-            let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
-            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
-            let pr_missing (c, missing) =
-              let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
-              let holes = List.init missing (fun _ -> hole) in
-              Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
-            in
-	    Feedback.msg_info
-	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");
-	    Feedback.msg_info
-	      (Pp.str "  Try " ++
-		 hov 8
-		 begin
-		   str "\"congruence with (" ++
-		     prlist_with_sep
-		     (fun () -> str ")" ++ spc () ++ str "(")
-		     pr_missing
-		     terms_to_complete ++
-		     str ")\","
-		 end ++
-		 Pp.str "  replacing metavariables by arbitrary terms.");
-	    Tacticals.New.tclFAIL 0 (str "Incomplete")
+      let open Glob_term in
+      let env = Proofview.Goal.env gl in
+      let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+      let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+      let pr_missing (c, missing) =
+        let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+        let holes = List.init missing (fun _ -> hole) in
+        Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+      in
+            let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+                    ++ fnl () ++
+                    str "  Try " ++
+                    hov 8
+                    begin
+                      str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
+                      pr_missing terms_to_complete ++ str ")\","
+                    end ++
+                    str "  replacing metavariables by arbitrary terms.") in
+      Tacticals.New.tclFAIL 0 msg
 	| Contradiction dis ->
       let env = Proofview.Goal.env gl in
             let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index e222fbc808..4f077b08b6 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -128,7 +128,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
-  -> {Feedback. msg_info (print_extraction_inline ()) }
+  -> {Feedback.msg_notice (print_extraction_inline ()) }
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -150,7 +150,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
-  -> { Feedback.msg_info (print_extraction_blacklist ()) }
+  -> { Feedback.msg_notice (print_extraction_blacklist ()) }
 END
 
 VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8a5c32b8b5..35cd10a1ff 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -83,7 +83,7 @@ END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> {
-    Feedback.msg_info
+    Feedback.msg_notice
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
 END
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 21d61d1f97..f7215a9d13 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
 END
 
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 455c8ab003..61cc77c42a 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -145,7 +145,7 @@ open Pp
 
 VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
 | [ "Show" "Obligation" "Tactic" ] -> {
-    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
+    Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
 END
 
 {
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
 let finish_timing ~prefix name =
   let tend = System.get_time () in
   let tstart = get_timer name in
-  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+  Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
                     System.fmt_time_difference tstart tend)
 
 (* ******************** *)
@@ -431,7 +431,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_info (to_string ~cutoff ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =
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 ())
 
 }