diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 451e0987b..5d3c149ab 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -1031,7 +1031,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ] +| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ] END |