From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 10:55:30 +0200
Subject: A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args
---
 tactics/hints.ml   | 19 ++++++++++++++-----
 tactics/tactics.ml | 14 +++++++++-----
 2 files changed, 23 insertions(+), 10 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9527191299..2c2b76412f 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_warning (str "the hint: eapply " ++ pr_lconstr c ++
+	    Feedback.msg_info (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,6 +743,12 @@ 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
@@ -754,9 +760,7 @@ let fresh_global_or_constr env sigma poly cr =
     else if Univ.ContextSet.is_empty ctx then (c, ctx)
     else begin
       if isgr then
-        Feedback.msg_warning (str"Using polymorphic hint " ++
-		     pr_hint_term env sigma ctx cr ++ str" monomorphically" ++
-		     str" use Polymorphic Hint to use it polymorphically.");
+        warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
       Lib.add_anonymous_leaf (input_context_set ctx);
       (c, Univ.ContextSet.empty)
     end
@@ -1389,10 +1393,15 @@ 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
-  let () = Feedback.msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
+  warn_non_imported_hint (hint,mp);
   Proofview.tclUNIT x
 
 let run_hint tac k = match !warn_hint with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f3e117f8c3..cf842d6f19 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2976,13 +2976,17 @@ 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
-    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)
+    warn_unused_intro_pattern names
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous
-- 
cgit v1.2.3