diff options
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 |