diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 43 |
1 files changed, 13 insertions, 30 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 488ca5f5d0..d59e62640e 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}, |