2 files changed, 13 insertions, 13 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index af1ed0f29f..75a9089216 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1335,21 +1335,20 @@ command \texttt{Functional Scheme} which builds induction
 principles following the recursive structure of (possibly
 mutually recursive) functions.
 
-\texttt{functional induction} does not work on dependently typed
-function yet. It may also fail on functions built by certain
-tactics.
+\Rem \texttt{functional induction} does not work on polymorphic
+and dependently typed functions yet. It may also fail on
+functions built by certain tactics.
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}}
 
 \section{Equality}
-These tactics use the equality {\tt
-eq:(A:Set)A->A->Prop} defined in file {\tt Logic.v} and the equality
-{\tt eqT:(A:Type)A->A->Prop} defined in file {\tt
-Logic\_Type.v} (see section \ref{Equality}). They
-are simply written {\tt t=u} and {\tt t==u},
-respectively.  In the following, the notation {\tt
-t=u} will represent either one of these two
-equalities.
+
+These tactics use the equality {\tt eq:(A:Set)A->A->Prop} defined
+in file {\tt Logic.v} and the equality {\tt
+  eqT:(A:Type)A->A->Prop} defined in file {\tt Logic\_Type.v} (see
+section \ref{Equality}). They are simply written {\tt t=u} and
+{\tt t==u}, respectively.  In the following, the notation {\tt
+  t=u} will represent either one of these two equalities.
 
 \subsection{\tt rewrite \term}
 \label{rewrite}
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 8503630a5c..57b779281f 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -359,8 +359,9 @@ a induction principle, so be warned that each time it is used, a
 term mimicking the structure of \texttt{div2} (roughly the size
 of {\tt div2\_ind}) is built. Using \texttt{Functional Scheme} is
 generally faster and less memory consuming.  On the other hand
-\texttt{functional induction} performs some extra simplification
-steps that \texttt{Functional Scheme} does not.
+\texttt{functional induction} performs some extra simplifications
+that \texttt{Functional Scheme} does not, and as it is a tactic
+it can be used in tactic definitions.