RefMan-tac: fix a few glitches concerning the documentation of eqn:

 These were introduced during Guillaume's backport to trunk of its
 improved tactic documentation

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

1 files changed, 13 insertions, 30 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 488ca5f5d..d59e62640 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1471,21 +1471,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   (see Section~\ref{intros-pattern}), in particular {\tt ?} can be
   used to let Coq generate a fresh name.
 
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn}
-
-  This behaves as {\tt destruct {\term}} but adds an equation between
-  {\term} and the value that {\term} takes in each of the possible
-  cases.  The name of the equation is chosen by Coq. If
-  {\disjconjintropattern} is simply {\tt []}, it is automatically considered
-  as a disjunctive pattern of the appropriate size.
-
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn:~{\namingintropattern}}
-
-  This behaves as {\tt destruct {\term} as
-    {\disjconjintropattern} \_eqn} but use {\namingintropattern} to
-  name the equation (see Section~\ref{intros-pattern}). Note that spaces
-  can generally be removed around {\tt \_eqn}.
-
 \item{\tt destruct {\term} with \bindinglist}
 
   This behaves like \texttt{destruct {\term}} providing explicit
@@ -1513,16 +1498,15 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   occurrence clause whose syntax and behavior is described in
   Section~\ref{Occurrences clauses}.
 
-%  When an occurrence clause is given, an equation between {\term} and
-%  the value it gets in each case of the analysis is added to the
-%  context of the subgoals corresponding to the cases (even
-%  if no clause {\tt as {\namingintropattern}} is given).
-
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn:~{\namingintropattern}  using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn:~{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$}
+        as {\disjconjintropattern} eqn:{\namingintropattern}
+        using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$}
+        as {\disjconjintropattern} eqn:{\namingintropattern}
+        using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
   These are the general forms of {\tt destruct} and {\tt edestruct}.
-  They combine the effects of the {\tt with}, {\tt as}, {\tt using},
+  They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
 \item{\tt case \term}\label{case}\tacindex{case}
@@ -1691,13 +1675,12 @@ induction n.
   occurrence clause whose syntax and behavior is described in
   Section~\ref{Occurrences clauses}.
 
-  When an occurrence clause is given, an equation between {\term} and
-  the value it gets in each case of the induction is added to the
-  context of the subgoals corresponding to the induction cases (even
-  if no clause {\tt eqn:{\namingintropattern}} is given).
-
-\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$}
+       as {\disjconjintropattern} eqn:{\namingintropattern}
+       using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$}
+       as {\disjconjintropattern} eqn:{\namingintropattern}
+       using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
   These are the most general forms of {\tt induction} and {\tt
   einduction}.  It combines the effects of the {\tt with}, {\tt as},