Move reflexivity, symmetry, and transitivity, next to f_equal, in the documentation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15812 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 32 insertions, 33 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 67830750e..488ca5f5d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2671,39 +2671,6 @@ n}| assumption || symmetry; try assumption]}.
 
 \end{Variants}
 
-\subsection{\tt reflexivity}
-\label{reflexivity}
-\tacindex{reflexivity}
-
-This tactic applies to a goal that has the form {\tt t=u}. It checks
-that {\tt t} and {\tt u} are convertible and then solves the goal.
-It is equivalent to {\tt apply refl\_equal}.
-
-\begin{ErrMsgs}
-\item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with \dots}
-\end{ErrMsgs}
-
-\subsection{\tt symmetry}
-\tacindex{symmetry}
-
-This tactic applies to a goal that has the form {\tt t=u} and changes it
-into {\tt u=t}.
-
-\begin{Variants}
-\item {\tt symmetry in \ident} \tacindex{symmetry in}
-
-If the statement of the hypothesis {\ident} has the form {\tt t=u},
-the tactic changes it to {\tt u=t}.
-\end{Variants}
-
-\subsection{\tt transitivity \term}
-\tacindex{transitivity}
-
-This tactic applies to a goal that has the form {\tt t=u}
-and transforms it into the two subgoals
-{\tt t={\term}} and {\tt {\term}=u}.
-
 \subsection{\tt subst \ident}
 \tacindex{subst}
 
@@ -4156,6 +4123,38 @@ subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst
 these subgoals, the simple ones (e.g. provable by
 reflexivity or congruence) are automatically solved by {\tt f\_equal}.
 
+\subsection{\tt reflexivity}
+\label{reflexivity}
+\tacindex{reflexivity}
+
+This tactic applies to a goal that has the form {\tt t=u}. It checks
+that {\tt t} and {\tt u} are convertible and then solves the goal.
+It is equivalent to {\tt apply refl\_equal}.
+
+\begin{ErrMsgs}
+\item \errindex{The conclusion is not a substitutive equation}
+\item \errindex{Impossible to unify \dots\ with \dots}
+\end{ErrMsgs}
+
+\subsection{\tt symmetry}
+\tacindex{symmetry}
+
+This tactic applies to a goal that has the form {\tt t=u} and changes it
+into {\tt u=t}.
+
+\begin{Variants}
+\item {\tt symmetry in \ident} \tacindex{symmetry in}
+
+If the statement of the hypothesis {\ident} has the form {\tt t=u},
+the tactic changes it to {\tt u=t}.
+\end{Variants}
+
+\subsection{\tt transitivity \term}
+\tacindex{transitivity}
+
+This tactic applies to a goal that has the form {\tt t=u}
+and transforms it into the two subgoals
+{\tt t={\term}} and {\tt {\term}=u}.
 
 \section{Equality and inductive sets}