diff options
| author | Guillaume Melquiond | 2018-10-31 14:49:58 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2018-11-06 10:51:56 +0100 |
| commit | 0f03707044822631160d516d65a80fc4bc45d104 (patch) | |
| tree | 36294c7d8bfd56fed864437c038eddf6df44f6e0 /doc/sphinx/proof-engine | |
| parent | 1aa71f100ddd5e3651a7d6e4adf0ebba5ae5fdee (diff) | |
Improve rendering of the credits.
This mostly fixes text that was italicized instead of teletyped. When
possible, tactic names have been made to point to their documentation.
Also, the date of the 8.9 release has been proactively changed to
November.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 26f4ec6242..457f9b2efa 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2226,6 +2226,7 @@ and an explanation of the underlying technique. :n:`inversion @ident using @ident`. .. tacv:: inversion_sigma + :name: inversion_sigma This tactic turns equalities of dependent pairs (e.g., :g:`existT P x p = existT P y q`, frequently left over by inversion on @@ -2369,7 +2370,7 @@ and an explanation of the underlying technique. assumption. Qed. -.. tacn:: fix ident num +.. tacn:: fix @ident @num :name: fix This tactic is a primitive tactic to start a proof by induction. In |