diff options
| author | coqbot-app[bot] | 2021-03-08 20:22:04 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-08 20:22:04 +0000 |
| commit | b55216ab3509f48e45aac035f1b799529d068f51 (patch) | |
| tree | 56deddf678f024309b084951b8f6997d7e303d3d /doc/sphinx/addendum/program.rst | |
| parent | 4a0cf0f3fb4a1a57627f22897030771b2921ce85 (diff) | |
| parent | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (diff) | |
Merge PR #13707: Convert 2nd part of rewriting chapter to prodn
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 8f2b51ccce..a011c81f15 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -149,7 +149,7 @@ when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts :cmd:`Definition` and :cmd:`Fixpoint` -in that they define constants. However, they may require the user to +in that they define :term:`constants <constant>`. However, they may require the user to prove some goals to construct the final definitions. @@ -173,7 +173,7 @@ term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to set of obligations generated during the interpretation of :n:`@term__0` and the aforementioned coercion derivation are solved. -.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` +.. seealso:: Sections :ref:`controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: |