Revising r16550 about providing intro patterns for applying injection:

- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

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

1 files changed, 13 insertions, 9 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2382175601..9aa53eb2be 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -776,11 +776,12 @@ either:
   \item the pattern \texttt{?\ident}
   \item an identifier
   \end{itemize}
-\item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
+\item a {\em composite introduction pattern}, i.e. either one of:
   \begin{itemize}
   \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
   \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
+  \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
   \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
    for sequence of right-associative binary constructs
   \end{itemize}
@@ -822,14 +823,17 @@ introduction pattern~$p$:
   of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
   $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
   $p_n$]});
-\item as a special case, if the product is over an equality type, then
-  a pattern of the form {\tt [$p_{1}$ \dots\ $p_n$]} or of the form
-  {\tt ($p_1$, \ldots, $p_n$)} applies {\tt injection} instead of {\tt
-    destruct} on the hypothesis and use the patterns $p_1$, \ldots,
-  $p_n$ on the hypotheses generated by {\tt injection} (see
-  Section~\ref{injection}); if the number of patterns is smaller than
-  the number of hypotheses generated, the pattern \texttt{?} is used
-  to complete the list;
+\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}
+  (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
+  used on the hypotheses generated by {\tt injection}; if the number
+  of patterns is smaller than the number of hypotheses generated, the
+  pattern \texttt{?} is used to complete the list;
+  %TODO!
+  %if {\tt discriminate} is applicable, the list of patterns $p_{1}$
+  %\dots\ $p_n$ is supposed to be empty;
 \item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)}
   is a shortcut for introduction via
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the