diff options
| author | Clément Pit-Claudel | 2019-05-20 16:02:57 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-22 14:44:46 -0400 |
| commit | 0a73aa4c4474bafb43b250fb86fb6eae3dfd1219 (patch) | |
| tree | 17ddeb5f6148fb456d5cc40d6dc21bf8263eb393 /doc/sphinx/addendum/program.rst | |
| parent | 54268ad2a17527b628436e662d0111cfb0c9a018 (diff) | |
[refman] Add more missing @ signs
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 4 |
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} |