diff options
| author | Clément Pit-Claudel | 2018-12-03 12:12:45 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-12-03 12:12:45 -0500 |
| commit | fe81b1a6f813fe21f0cc21ede761acae64c7b026 (patch) | |
| tree | aa41144b404abccb24513ed6fe05a3b379e55fdf /doc/sphinx/addendum/program.rst | |
| parent | 0f0caf884d54fd81e0394dcedf0b77aaf8b19045 (diff) | |
| parent | c01490985794c3ddaad4b9fa2b951a0b8599bdea (diff) | |
Merge PR #9121: Closes #9118: single backticks are made equivalent to double backticks; try to fix all misuses.
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 e153c7cbe2..429dcbee69 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -181,7 +181,7 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term The optional order annotation follows the grammar: |