From 0f03707044822631160d516d65a80fc4bc45d104 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 31 Oct 2018 14:49:58 +0100
Subject: 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.
---
 doc/sphinx/proof-engine/tactics.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

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
-- 
cgit v1.2.3