diff options
| author | Théo Zimmermann | 2020-09-11 12:25:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-11 12:29:25 +0200 |
| commit | 6abc0f4de27e4c0ecbbc7736388682abe21ebd7f (patch) | |
| tree | 885abc171c9dcfe53ae92559ec594afbe57efcec /doc/sphinx/addendum/program.rst | |
| parent | a764c64bfe3d3c604931087459fb6f4ae727cbea (diff) | |
Minimal changes to make the refman compatible with Sphinx 3.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b5618c5721..3d36c5c50f 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -196,12 +196,9 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition } - The optional order annotation follows the grammar: - - .. productionlist:: orderannot - order : measure `term` [ `term` ] | wf `term` `ident` + The optional :n:`@fixannot` annotation can be one of: + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on any subset of the arguments and the optional term |