aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum/program.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
-rw-r--r--doc/sphinx/addendum/program.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 22ddcae584..45c74ab02a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified.
Displays all remaining obligations.
-.. cmd:: Obligation num {? of @ident}
+.. cmd:: Obligation @num {? of @ident}
- Start the proof of obligation num.
+ Start the proof of obligation :token:`num`.
.. cmd:: Next Obligation {? of @ident}