- Fixed many "Theorem with" bugs.

- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".



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

1 files changed, 37 insertions, 10 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 01ea532e6..ba106e240 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -600,14 +600,31 @@ in the list of subgoals remaining to prove.
   This tactic behaves like \texttt{assert} but applies {\tac}
   to solve the subgoals generated by \texttt{assert}.
 
-\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
+\item \texttt{assert {\form} as {\intropattern}\tacindex{assert as}}
 
-   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
+  If {\intropattern} is a naming introduction pattern (see
+  Section~\ref{intros-pattern}), the hypothesis is named after this
+  introduction pattern (in particular, if {\intropattern} is {\ident},
+  the tactic behaves like \texttt{assert ({\ident} : {\form})}).
 
-\item \texttt{pose proof {\term} as {\ident}\tacindex{pose proof}}
+  If {\intropattern} is a disjunctive/conjunctive introduction
+  pattern, the tactic behaves like \texttt{assert {\form}} then destructing the
+  resulting hypothesis using the given introduction pattern.
 
-  This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where
-  \texttt{T} is the type of {\term}. 
+\item \texttt{assert {\form} as {\intropattern} by {\tac}}
+
+  This combines the two previous variants of {\tt assert}.
+
+\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
+
+  This tactic behaves like \texttt{assert T as {\intropattern} by
+  exact {\term}} where \texttt{T} is the type of {\term}.
+
+  In particular, \texttt{pose proof {\term} as {\ident}} behaves as
+  \texttt{assert ({\ident}:T) by exact {\term}} (where \texttt{T} is
+  the type of {\term}) and \texttt{pose proof {\term} as
+  {\disjconjintropattern}\tacindex{pose proof}} behaves
+  like \texttt{destruct {\term} as {\disjconjintropattern}}.
 
 \item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)\tacindex{specialize}} \\
       {\tt specialize {\ident} with \bindinglist}
@@ -681,6 +698,17 @@ This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
 {\ident}} but turns unresolved bindings into existential variables, if
 any, instead of failing.
 
+\item {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in
+{\ident}} then destructs the hypothesis {\ident} along
+{\disjconjintropattern} as {\tt destruct {\ident} as
+{\disjconjintropattern}} would.
+
+\item {\tt eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+
 \end{Variants}
 
 \subsection{\tt generalize \term
@@ -1779,10 +1807,6 @@ last introduced hypothesis.
   as existential variables to be inferred later, in the same way as
   {\tt eapply} does (see Section~\ref{eapply-example}).
 
-\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
-
-  This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
-
 \item{\tt destruct {\term$_1$} using {\term$_2$}}\\
      {\tt destruct {\term$_1$} using {\term$_2$} with {\bindinglist}}
 
@@ -1855,6 +1879,9 @@ last introduced hypothesis.
 \subsection{\tt intros {\intropattern} {\ldots} {\intropattern}
 \label{intros-pattern}
 \tacindex{intros \intropattern}}
+\index{Introduction patterns}
+\index{Naming introduction patterns}
+\index{Disjunctive/conjunctive introduction patterns}
 
 This extension of the tactic {\tt intros} combines introduction of
 variables or hypotheses and case analysis. An {\em introduction pattern} is
@@ -4136,7 +4163,7 @@ principles, closer to the definition written by the user.
 
 
 \section{Simple tactic macros
-\index{tactic macros}
+\index{Tactic macros}
 \comindex{Tactic Definition}
 \label{TacticDefinition}}