diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 11d62b60a..ce934871f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -864,16 +864,17 @@ introduction pattern~$p$: expects the product to be over an inductive type whose number of constructors is $n$ (or more generally over a type of conclusion an inductive type built from $n$ constructors, - e.g. {\tt C -> A\textbackslash/B if $n=2$}): it destructs the introduced + e.g. {\tt C -> A\textbackslash/B} with $n=2$ since {\tt + A\textbackslash/B} has 2 constructors): it destructs the introduced hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and applies on each generated subgoal the corresponding tactic; \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive - pattern is part of a sequence of patterns and is not the last - pattern of the sequence, then {\Coq} completes the pattern so that all - the argument of the constructors of the inductive type are - introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H} - applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as - the list of patterns {\tt [$\,$|$\,$?$\,$] H}); + pattern is part of a sequence of patterns, then {\Coq} completes the + pattern so that all the arguments of the constructors of the + inductive type are introduced (for instance, the list of patterns + {\tt [$\;$|$\;$] H} applied on goal {\tt forall x:nat, x=0 -> 0=x} + behaves the same as the list of patterns {\tt [$\,$|$\,$?$\,$] H}, + up to one exception explained in the Remark below); \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots, $p_n$)} expects the goal to be a product over an inductive type $I$ with a single constructor that itself has at least $n$ arguments: it @@ -887,10 +888,10 @@ introduction pattern~$p$: {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an - hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be + hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be introduced via pattern {\tt (a \& x \& b \& c \& d)}; \item if the product is over an equality type, then a pattern of the - form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection} + form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection} (see Section~\ref{injection}) or {\tt discriminate} (see Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are @@ -950,6 +951,7 @@ Abort. \Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to \texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons: +\label{bracketing-last} \begin{itemize} \item A wildcard pattern never succeeds when applied isolated on a dependent product, while it succeeds as part of a list of @@ -971,6 +973,13 @@ Show 2. \end{itemize} +This later behavior can be avoided by setting the following option: + +\begin{quote} +\optindex{Bracketing Last Introduction Pattern} +{\tt Set Bracketing Last Introduction Pattern} +\end{quote} + \subsection{\tt clear \ident} \tacindex{clear} \label{clear} |