diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b5618c5721..c6a4b4fe1a 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 @@ -306,9 +303,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation @num {? of @ident} +.. cmd:: Obligation @natural {? of @ident} - Start the proof of obligation :token:`num`. + Start the proof of obligation :token:`natural`. .. cmd:: Next Obligation {? of @ident} |