- 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

2 files changed, 39 insertions, 12 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index c7f6bf02e..1b6efc582 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -682,8 +682,8 @@ tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
 improved the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
 particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
-team, the INRIA-Microsoft Mathematical Components team, the
-Foundations group at Radbout university in Nijmegen, reporters of bugs
+team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
+the Foundations group at Radbout university in Nijmegen, reporters of bugs
 and participants to the Coq-Club mailing list.
 
 \begin{flushright}
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}}