diff options
| author | Théo Zimmermann | 2018-11-06 14:07:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-06 14:07:57 +0100 |
| commit | 11879733b7f2d2554bcfc7a851479ec8adc3e97e (patch) | |
| tree | 2800a5fc49e75c4232d4c0bb4d1abee05dd00d99 /doc/sphinx/proof-engine | |
| parent | f086374af55037f9a977258652b69ab7511401a4 (diff) | |
| parent | 0f03707044822631160d516d65a80fc4bc45d104 (diff) | |
Merge PR #8884: Improve rendering of the credits.
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 |