diff --git a/docs/grub.texi b/docs/grub.texi
index 5383aa29a..f9299041f 100644
--- a/docs/grub.texi
+++ b/docs/grub.texi
@@ -1315,33 +1315,8 @@ associated menu entry immediately.  If the timeout expires before either of
 these happens, it will boot the default entry.  In the @samp{countdown}
 case, it will show a one-line indication of the remaining time.
 
-@item GRUB_HIDDEN_TIMEOUT
-Wait this many seconds before displaying the menu.  If @key{ESC} is pressed
-during that time, display the menu and wait for input according to
-@samp{GRUB_TIMEOUT}.  If a hotkey associated with a menu entry is pressed,
-boot the associated menu entry immediately.  If the timeout expires before
-either of these happens, display the menu for the number of seconds
-specified in @samp{GRUB_TIMEOUT} before booting the default entry.
-
-If you set @samp{GRUB_HIDDEN_TIMEOUT}, you should also set
-@samp{GRUB_TIMEOUT=0} so that the menu is not displayed at all unless
-@key{ESC} is pressed.
-
-This option is unset by default, and is deprecated in favour of the less
-confusing @samp{GRUB_TIMEOUT_STYLE=countdown} or
-@samp{GRUB_TIMEOUT_STYLE=hidden}.
-
-@item GRUB_HIDDEN_TIMEOUT_QUIET
-In conjunction with @samp{GRUB_HIDDEN_TIMEOUT}, set this to @samp{true} to
-suppress the verbose countdown while waiting for a key to be pressed before
-displaying the menu.
-
-This option is unset by default, and is deprecated in favour of the less
-confusing @samp{GRUB_TIMEOUT_STYLE=countdown}.
-
 @item GRUB_DEFAULT_BUTTON
 @itemx GRUB_TIMEOUT_BUTTON
-@itemx GRUB_HIDDEN_TIMEOUT_BUTTON
 @itemx GRUB_BUTTON_CMOS_ADDRESS
 Variants of the corresponding variables without the @samp{_BUTTON} suffix,
 used to support vendor-specific power buttons.  @xref{Vendor power-on keys}.
@@ -1516,6 +1491,44 @@ Each module will be loaded as early as possible, at the start of
 
 @end table
 
+The following options are still accepted for compatibility with existing
+configurations, but have better replacements:
+
+@table @samp
+@item GRUB_HIDDEN_TIMEOUT
+Wait this many seconds before displaying the menu.  If @key{ESC} is pressed
+during that time, display the menu and wait for input according to
+@samp{GRUB_TIMEOUT}.  If a hotkey associated with a menu entry is pressed,
+boot the associated menu entry immediately.  If the timeout expires before
+either of these happens, display the menu for the number of seconds
+specified in @samp{GRUB_TIMEOUT} before booting the default entry.
+
+If you set @samp{GRUB_HIDDEN_TIMEOUT}, you should also set
+@samp{GRUB_TIMEOUT=0} so that the menu is not displayed at all unless
+@key{ESC} is pressed.
+
+This option is unset by default, and is deprecated in favour of the less
+confusing @samp{GRUB_TIMEOUT_STYLE=countdown} or
+@samp{GRUB_TIMEOUT_STYLE=hidden}.
+
+@item GRUB_HIDDEN_TIMEOUT_QUIET
+In conjunction with @samp{GRUB_HIDDEN_TIMEOUT}, set this to @samp{true} to
+suppress the verbose countdown while waiting for a key to be pressed before
+displaying the menu.
+
+This option is unset by default, and is deprecated in favour of the less
+confusing @samp{GRUB_TIMEOUT_STYLE=countdown}.
+
+@item GRUB_HIDDEN_TIMEOUT_BUTTON
+Variant of @samp{GRUB_HIDDEN_TIMEOUT}, used to support vendor-specific power
+buttons.  @xref{Vendor power-on keys}.
+
+This option is unset by default, and is deprecated in favour of the less
+confusing @samp{GRUB_TIMEOUT_STYLE=countdown} or
+@samp{GRUB_TIMEOUT_STYLE=hidden}.
+
+@end table
+
 For more detailed customisation of @command{grub-mkconfig}'s output, you may
 edit the scripts in @file{/etc/grub.d} directly.
 @file{/etc/grub.d/40_custom} is particularly useful for adding entire custom