Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

2 files changed, 10 insertions, 23 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2c2b76412f..9527191299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -708,7 +708,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
+	    Feedback.msg_warning (str "the hint: eapply " ++ pr_lconstr c ++
 	    str " will only be used by eauto");
           (Some hd,
            { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
@@ -743,12 +743,6 @@ let input_context_set : Univ.ContextSet.t -> Libobject.obj =
       discharge_function = (fun (_,a) -> Some a);
       classify_function = (fun a -> Keep a) }
 
-let warn_polymorphic_hint =
-  CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
-         (fun hint -> strbrk"Using polymorphic hint " ++ hint ++
-                        str" monomorphically" ++
-                        strbrk" use Polymorphic Hint to use it polymorphically.")
-
 let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
@@ -760,7 +754,9 @@ let fresh_global_or_constr env sigma poly cr =
     else if Univ.ContextSet.is_empty ctx then (c, ctx)
     else begin
       if isgr then
-        warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
+        Feedback.msg_warning (str"Using polymorphic hint " ++
+		     pr_hint_term env sigma ctx cr ++ str" monomorphically" ++
+		     str" use Polymorphic Hint to use it polymorphically.");
       Lib.add_anonymous_leaf (input_context_set ctx);
       (c, Univ.ContextSet.empty)
     end
@@ -1393,15 +1389,10 @@ let print_mp mp =
 
 let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
 
-let warn_non_imported_hint =
-  CWarnings.create ~name:"non-imported-hint" ~category:"automation"
-         (fun (hint,mp) ->
-          strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
-
 let warn h x =
   let hint = pr_hint h in
   let (mp, _, _) = KerName.repr h.uid in
-  warn_non_imported_hint (hint,mp);
+  let () = Feedback.msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
   Proofview.tclUNIT x
 
 let run_hint tac k = match !warn_hint with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cf842d6f19..f3e117f8c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2976,17 +2976,13 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
  *)
 
-let warn_unused_intro_pattern =
-  CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
-         (fun names ->
-          strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-          ++ str": " ++ prlist_with_sep spc 
-         (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
-
 let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then
-    warn_unused_intro_pattern names
+    Feedback.msg_warning
+      (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
+       ++ str": " ++ prlist_with_sep spc 
+	 (Miscprint.pr_intro_pattern 
+	    (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous