diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 24d4d7e81..dfa09085d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4294,6 +4294,7 @@ assistant.  It supports most of the generic features of Proof General.
 @menu
 * Coq-specific commands::
 * Using the Coq project file::
+* Proof using annotations::
 * Multiple File Support::
 * Editing multiple proofs::
 * User-loaded tactics::