diff options
| author | Théo Zimmermann | 2018-11-30 22:54:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-03 13:59:38 +0100 |
| commit | 5e58df994c31776563d8832c0eb65e51d24e7652 (patch) | |
| tree | 91b2b8e7a1a2fe500e73b5590eed36981c7f643a /doc/sphinx/addendum/program.rst | |
| parent | 65d35e1294419e7f09903dace816750fd8d362eb (diff) | |
A few fixes of unexisting tokens.
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: |