diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a48bbf89d..bbee39c3d 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -150,7 +150,7 @@ let alarm what internal msg = | UserAutomaticRequest | InternalTacticRequest -> (if debug then - Feedback.msg_warning + Feedback.msg_debug (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None | _ -> Some msg @@ -295,6 +295,11 @@ let declare_rewriting_schemes ind = (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind end +let warn_cannot_build_congruence = + CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes" + (fun () -> + strbrk "Cannot build congruence scheme because eq is not found") + let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if @@ -303,7 +308,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else - Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found") + warn_cannot_build_congruence () end let declare_sym_scheme ind = |