Making the behavior of "injection ... as ..." more natural:

- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
  if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.

However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".

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

1 files changed, 15 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 432ff52796..2382175601 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -822,6 +822,14 @@ 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 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
@@ -2118,7 +2126,13 @@ introduced hypothesis.
 \tacindex{injection \dots\ as}
 
 These variants apply \texttt{intros} \nelistnosep{\intropattern} after
-the call to \texttt{injection} or \texttt{einjection}.
+the call to \texttt{injection} or \texttt{einjection} so that all
+equalities generated are moved in the context of hypotheses. The
+number of {\intropattern} must not exceed the number of equalities
+newly generated. If it is smaller, fresh names are automatically
+generated to adjust the list of {\intropattern} to the number of new
+equalities. The original equality is erased if it corresponds to an
+hypothesis.
 
 \end{Variants}