aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/indschemes.ml')
-rw-r--r--toplevel/indschemes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 367425546..f995a390c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
| UserAutomaticRequest
| InternalTacticRequest ->
(if debug then
- msg_warning
+ Feedback.msg_warning
(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
| _ -> Some msg
@@ -303,7 +303,7 @@ let declare_congr_scheme ind =
then
ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
else
- msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
+ Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
end
let declare_sym_scheme ind =