From e02120ed6580733db2276f0c11b4f432ea670ee3 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert rewriting and proof-mode chapters to prodn

---
 doc/sphinx/using/libraries/funind.rst | 2 --
 1 file changed, 2 deletions(-)

(limited to 'doc/sphinx/using/libraries')

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 93571ecebb..0f0edc6bdd 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -170,7 +170,6 @@ Tactics
 -------
 
 .. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern }
-   :name: functional induction
 
    Performs case analysis and induction following the definition of a function
    :token:`qualid`, which must be fully applied to its arguments as part of
@@ -221,7 +220,6 @@ Tactics
       :undocumented:
 
 .. tacn:: functional inversion {| @ident | @natural } {? @qualid }
-   :name: functional inversion
 
    Performs inversion on hypothesis
    :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or
-- 
cgit v1.2.3