diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 19 | ||||
| -rw-r--r-- | tactics/tactics.ml | 14 |
2 files changed, 23 insertions, 10 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 952719129..2c2b76412 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 f3e117f8c..cf842d6f1 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 |