Use CWarnings infrastructure for warnings

src/equations_common.ml

@@ -41,6 +41,7 @@ let equations_derive_equations = ref true
 let equations_derive_eliminator = ref true
 
 let depr_with_k = Deprecation.make ~since:"equations v1.2" ()
+let equations_category = CWarnings.create_category ~name:"equations" ()
 
 let () = Goptions.declare_bool_option {
   Goptions.optdepr  = Some depr_with_k;

src/equations_common.mli

@@ -23,6 +23,8 @@ val equations_derive_eliminator : bool ref
 val debug : bool ref
 val equations_debug : (unit -> Pp.t) -> unit
 
+val equations_category : CWarnings.category
+
 val ppenv_sigma : (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a -> unit
 
 (* Common flags *)

src/principles.ml

@@ -727,6 +727,9 @@ let subst_protos info s gr =
   else Hints.hint_globref gr
   [@@ocaml.warning "-3"]
 
+let wf_hint_warning = CWarnings.create ~name:"wf-obligation-cannot-be-used" ~category:equations_category
+  Pp.(fun (gr, msg) -> str"The decreasing recursive call obligation " ++ Printer.pr_global gr ++ str" could not be defined as a hint: " ++ fnl () ++ msg)
+
 let declare_wf_obligations s info =
   let make_resolve gr =
     equations_debug Pp.(fun () -> str"Declaring wf obligation " ++ Printer.pr_global gr);
@@ -741,7 +744,7 @@ let declare_wf_obligations s info =
             [dbname]
             (Hints.HintsResolveEntry [hint])
       with CErrors.UserError msg (* Cannot be used as a hint *) ->
-        Feedback.msg_warning msg)
+        wf_hint_warning (GlobRef.ConstRef obl, msg))
     info.comp_obls
 
 let map_fix_subst evd ctxmap s =
@@ -1301,6 +1304,10 @@ let mkConj evd sort x y =
   let prod = get_efresh logic_product evd in
     mkApp (prod, [| x; y |])
 
+let functional_proof_warning = 
+  CWarnings.create ~name:"functional-induction-derivation-failure" ~category:equations_category
+    Pp.(fun msg -> str"Functional induction/elimination principle could not be proved automatically: " ++ msg)
+
 let declare_funind ~pm info alias env evd is_rec protos progs
                    ind_stmts all_stmts sign inds kn comb sort f split =
   let poly = is_polymorphic info.term_info in
@@ -1366,8 +1373,7 @@ let declare_funind ~pm info alias env evd is_rec protos progs
         CErrors.user_err Pp.(str"Functional elimination principle could not be proved automatically: " ++
                              Himsg.explain_pretype_error env sigma tyerr)
       | e ->
-        Feedback.msg_warning Pp.(str "Functional elimination principle could not be proved automatically: "
-                                 ++ fnl () ++ CErrors.print e);
+        functional_proof_warning Pp.(fnl () ++ CErrors.print e);
         pm
     in
     let evd = Evd.from_env env in
@@ -1414,8 +1420,7 @@ let declare_funind ~pm info alias env evd is_rec protos progs
     match res with
     | Declare.Obls.Defined gr -> ()
     | Declare.Obls.Remain _  ->
-      Feedback.msg_warning Pp.(str "Functional induction principle could not be proved automatically, it \
-        is left as an obligation.")
+      functional_proof_warning Pp.(str "it is left as an obligation.")
     | Declare.Obls.Dependent -> (* Only 1 obligation *) assert false
   in
   let tac = (ind_fun_tac is_rec f info id !nested_statements progs) in
@@ -1424,9 +1429,8 @@ let declare_funind ~pm info alias env evd is_rec protos progs
     CErrors.user_err Pp.(str"Functional induction principle could not be proved automatically: " ++
                          Himsg.explain_pretype_error env !evd
                            (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
-     | e when CErrors.noncritical e ->
-       Feedback.msg_warning Pp.(str "Functional induction principle could not be proved automatically: " ++ fnl () ++
-                                CErrors.print e);
+    | e when CErrors.noncritical e ->
+       functional_proof_warning Pp.(fnl () ++ CErrors.print e);
        launch_ind ~pm (Proofview.tclUNIT ())
 
 let max_sort s1 s2 =

src/sigma_types.ml

@@ -290,6 +290,10 @@ let () =
             { derive_name = "Signature";
               derive_fn = make_derive_ind fn })
 
+let warn_auto_inline = 
+  CWarnings.create ~name:"signature-auto-inline" ~category:equations_category 
+    (fun msg -> msg) 
+
 let get_signature env sigma0 ty =
   try
     let sigma, (idx, _) =
@@ -314,7 +318,7 @@ let get_signature env sigma0 ty =
     let pind, args = Inductive.find_rectype env (to_constr sigma0 ty) in
     let sigma, pred, pars, _, valsig, ctx, _, _ =
       build_sig_of_ind env sigma0 (to_peuniverses pind) in
-    Feedback.msg_warning (str "Automatically inlined signature for type " ++
+    warn_auto_inline (str "Automatically inlined signature for type " ++
     Printer.pr_pinductive env sigma pind ++ str ". Use [Derive Signature for " ++
     Printer.pr_pinductive env sigma pind ++ str ".] to avoid this.");
     let indsig = pred in

src/splitting.ml

@@ -1039,12 +1039,11 @@ let warn_complete id =
   str "Equations definition " ++ Id.print id ++ str" is complete and requires no further proofs. " ++
   str "Use the \"Equations\" command to define it."
 
-let equations_cat = CWarnings.create_category ~name:"equations" ()
 
 let warn_complete = 
   CWarnings.create
     ~name:"equations-open-proof-complete"
-    ~category:equations_cat
+    ~category:equations_category
     ~default:CWarnings.Enabled
     warn_complete