diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index eb50e52dc7..1c3fdeb430 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,7 +135,7 @@ support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts -Definition (see Section `TODO-1.3.2-Definition`_) and Fixpoint (see Section `TODO-1.3.4-Fixpoint`_) +:cmd:`Definition` and :cmd:`Fixpoint` in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -174,7 +174,7 @@ Program Definition .. TODO refer to production in alias -See also: Sections `TODO-6.10.1-Opaque`_, `TODO-6.10.2-Transparent`_, `TODO-8.7.5-unfold`_ +See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: @@ -196,7 +196,7 @@ The optional order annotation follows the grammar: + :g:`wf R x` which is equivalent to :g:`measure x (R)`. The structural fixpoint operator behaves just like the one of |Coq| (see -Section `TODO-1.3.4-Fixpoint`_), except it may also generate obligations. It works +:cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. .. coqtop:: reset none |