diff options
Diffstat (limited to 'ltac/g_rewrite.ml4')
| -rw-r--r-- | ltac/g_rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index 395c2cd1b..29ffbed19 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -262,5 +262,5 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] END |