From a324162435df4666be99a3872717c84d93cca5ce Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Fri, 4 Apr 2014 22:06:16 +0200
Subject: fixing Function doc

---
 doc/refman/RefMan-tac.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 89d8df473b..7b09d84637 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1920,7 +1920,7 @@ dependent induction and an explanation of the underlying technique.
 \tacindex{functional induction}
 \label{FunInduction}
 
-The \emph{experimental} tactic \texttt{functional induction} performs
+The tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
 (see Section~\ref{Function}) or \texttt{Functional Scheme}
@@ -4284,9 +4284,10 @@ right to left.
 \label{inversion}}
 
 \subsection{\tt functional inversion \ident}
+\tacindex{functional inversion}
 \label{sec:functional-inversion}
 
-\texttt{functional inversion} is a \emph{highly} experimental tactic
+\texttt{functional inversion} is a tactic
 that performs inversion on hypothesis {\ident} of the form
 \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
   \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
-- 
cgit v1.2.3