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.

3 files changed, 23 insertions, 32 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 93a89330e3..893baad8c9 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -198,13 +198,15 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-       let names = pr_enum Libnames.pr_reference names in
-       let error = if do_observe () then (spc () ++ Errors.print e) else mt () in
-       warn_cannot_define_graph (names,error)
+	Feedback.msg_warning
+	  (str "Cannot define graph(s) for " ++
+	     h 1 (pr_enum Libnames.pr_reference names) ++
+	     if do_observe () then (spc () ++ Errors.print e) else mt ())
     | Defining_principle e ->
-       let names = pr_enum Libnames.pr_reference names in
-       let error = if do_observe () then Errors.print e else mt () in
-       warn_cannot_define_principle (names,error)
+	Feedback.msg_warning
+	  (str "Cannot define principle(s) for "++
+	     h 1 (pr_enum Libnames.pr_reference names) ++
+	     if do_observe () then Errors.print e else mt ())
     | _ -> raise e
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ebbb34e4c..1c5eb16218 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -227,11 +227,6 @@ let prepare_body ((name,_,args,types,_),_) rt =
 let process_vernac_interp_error e =
   fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
 
-let warn_funind_cannot_build_inversion =
-  CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
-    (fun e' -> strbrk "Cannot build inversion information" ++
-                 if do_observe () then (fnl() ++ Errors.print e') else mt ())
-
 let derive_inversion fix_names =
   try
     let evd' = Evd.from_env (Global.env ()) in 
@@ -274,20 +269,14 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      warn_funind_cannot_build_inversion e'
+      Feedback.msg_warning
+	(str "Cannot build inversion information" ++
+	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
   with e when Errors.noncritical e ->
-    let e' = process_vernac_interp_error e in
-    warn_funind_cannot_build_inversion e'
-
-let warn_cannot_define_graph =
-  CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
-    (fun (names,error) -> strbrk "Cannot define graph(s) for " ++
-      h 1 names ++ error)
-
-let warn_cannot_define_principle =
-  CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
-  (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++
-      h 1 names ++ error)
+      let e' = process_vernac_interp_error e in
+      Feedback.msg_warning
+	(str "Cannot build inversion information (early)" ++
+	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
 
 let warning_error names e =
   let e = process_vernac_interp_error e in
@@ -305,11 +294,15 @@ let warning_error names e =
   in
   match e with
     | Building_graph e ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_graph (names,e_explain e)
+      Feedback.msg_warning
+	(str "Cannot define graph(s) for " ++
+	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	   e_explain e)
     | Defining_principle e ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_principle (names,e_explain e)
+      Feedback.msg_warning
+	(str "Cannot define principle(s) for "++
+	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	   e_explain e)
     | _ -> raise e
 
 let error_error names e =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 1c27bdface..e720691406 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,9 +1,5 @@
 open Misctypes
 
-val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
-
-val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
-
 val do_generate_principle :  
   bool -> 
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->