diff options
| author | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
| commit | 8bd60579d4768793c849b9b4cd46f14d33d0f71d (patch) | |
| tree | 9fb0510584dae4f5416f8776b26cd7964ceb810f /doc/sphinx/addendum/program.rst | |
| parent | e3e8dfb4c2f30ed1c6715999e1f74914e7bc187b (diff) | |
| parent | feb9c50b5812a01e9dc60e2408f4f9f38986ce8c (diff) | |
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b410833d25..22ddcae584 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. -.. cmd:: {? Local|Global} Obligation Tactic := @tactic +.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations |