MAJ du manuel de référence

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

4 files changed, 52 insertions, 33 deletions

diff --git a/CHANGES b/CHANGES
index fb403a5cc8..7e69e8b06b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,15 +57,13 @@ Tactics
 - "rewrite ... in" now accepts a clause as place where to rewrite instead of 
   juste a simple hypothesis name. For instance: 
    rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
-   rewrite H in * |-  will do try rewrite H in Hi for all hypothesis Hi <> H 
-  (doc TODO).
+   rewrite H in * |-  will do try rewrite H in Hi for all hypothesis Hi <> H.
 - Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
-- Added "autorewrite with ... in hyp [using ...]" (doc TODO).
-- Tactic "replace" now accepts a "by" tactic clause (doc TODO).
-- Added "clear - id" to clear all hypotheses except the ones depending in id
-  (doc TODO).
+- Added "autorewrite with ... in hyp [using ...]".
+- Tactic "replace" now accepts a "by" tactic clause.
+- Added "clear - id" to clear all hypotheses except the ones depending in id.
 - The argument of Declare Left Step and Declare Right Step is now a term
-  (it used to be a reference) (doc TODO).
+  (it used to be a reference).
 - Omega now handles arbitrary precision integers.
 - Several bug fixes in Reflexive Omega (romega).
 - Idtac can now be left implicit in a [...|...] construct: for instance, 
@@ -77,13 +75,12 @@ Tactics
   used to solve unresolved subterms of term arguments of tactics (doc TODO).
 - Better support for coercions to Sortclass in tactics expecting type 
   arguments.
-- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
-  (doc TODO).
+- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
   (doc TODO).
-- New introduction pattern "?" for letting Coq choose a name (doc TODO).
-- Added "eassumption" (doc TODO).
-- Added option 'using lemmas' to auto, trivial and eauto (doc TODO).
+- New introduction pattern "?" for letting Coq choose a name.
+- Added "eassumption".
+- Added option 'using lemmas' to auto, trivial and eauto.
 - Tactic "congruence" is now complete for its intended scope (ground
   equalities and inequalities with constructors). Furthermore, it
   tries to equates goal and hypotheses.
@@ -95,7 +92,7 @@ Tactics
   to see hidden occurrences).
 - Generalization of induction "induction x1...xn using scheme" where
   scheme is an induction principle with complex predicates (like the
-  ones generated by function induction) (doc TODO).
+  ones generated by function induction).
 - Some small Ltac tactics has been added to the standard library 
   (file Tactics.v):
   * f_equal : instead of using the different f_equalX lemmas
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d9e6007842..93a7406eb8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -149,6 +149,10 @@ usable in the proof development.
   its body. Otherwise said, this tactic turns a definition into an
   assumption.
 
+\item \texttt{clear - {\ident}.} 
+
+  This tactic clears all hypotheses except the ones depending in {\ident}.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -527,6 +531,10 @@ in the list of subgoals remaining to prove.
   This tactic behaves like \texttt{assert} but tries to apply {\tac}
   to any subgoals generated by \texttt{assert}.
 
+\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
+
+   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
+
 \end{Variants}
 
 % PAS CLAIR;
@@ -1125,6 +1133,11 @@ induction n.
 scheme of name {\qualid}. It does not expect that the type of
 {\term} is inductive.
 
+\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+
+  where {\qualid} is an induction principle with complex predicates
+  (like the ones generated by function induction).
+
 \item {\tt induction {\term} using {\qualid} as {\intropattern}}
 
   This combines {\tt induction {\term} using {\qualid}}
@@ -1308,6 +1321,7 @@ components of an hypothesis.
 An introduction pattern is either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
+\item the pattern \texttt{?}
 \item a variable
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
@@ -1319,6 +1333,8 @@ structure of the pattern given as argument:
 \begin{itemize}
 \item introduction on the wildcard do the introduction and then
   immediately clear (cf~\ref{clear}) the corresponding hypothesis;
+\item introduction on \texttt{?} do the introduction, and let Coq
+  choose a fresh name for the variable;
 \item introduction on a variable behaves like described in~\ref{intro}; 
 \item introduction over a
 list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
@@ -1509,7 +1525,10 @@ implicit type of $t$ and $u$.
 This tactic applies to any goal. The type of {\term}
 must have the form
 
-\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. 
+\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. 
+
+\noindent where \texttt{eq} is the Leibniz equality or a registered
+setoid equality.
 
 \noindent Then {\tt rewrite \term} replaces every occurrence of 
 \term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are
@@ -1536,10 +1555,14 @@ This happens if \term$_1$ does not occur in the goal.
 \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
-\item {\tt rewrite {\term} in {\ident}}
+\item {\tt rewrite {\term} in {\clause}}
   \tacindex{rewrite \dots\ in}\\
-  Analogous to  {\tt rewrite {\term}} but rewriting is done in the
-  hypothesis named {\ident}.
+  Analogous to {\tt rewrite {\term}} but rewriting is done following
+  {\clause} (similarly to \ref{Conversion-tactic}). For instance:
+  \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1;
+    rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do
+  \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <>
+    H}.
 
 \item {\tt rewrite -> {\term} in {\ident}}
   \tacindex{rewrite -> \dots\ in}\\
@@ -1656,12 +1679,12 @@ goal stating ``$eq$ {\term} {\term}$_1$''.
 Lemmas are added to the database using the command 
 \comindex{Declare Left Step}
 \begin{quote}
-{\tt Declare Left Step {\qualid}.}
+{\tt Declare Left Step {\term}.}
 \end{quote}
-where {\qualid} is the name of the lemma.
 
 The tactic is especially useful for parametric setoids which are not
-accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}).
+accepted as regular setoids for {\tt rewrite} and {\tt
+  setoid\_replace} (see chapter \ref{setoid_replace}).
 
 \tacindex{stepr}
 \comindex{Declare Right Step}
@@ -1677,7 +1700,7 @@ Lemmas are expected to be of the form
 $z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
 and are registered using the command
 \begin{quote}
-{\tt Declare Right Step {\qualid}.}
+{\tt Declare Right Step {\term}.}
 \end{quote}
 \end{Variants}
 
@@ -2746,7 +2769,7 @@ of the reengineering of the code, this tactic has also been completely revised
 to get a very compact and readable version.} carries out rewritings according
 the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
 
- Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
+Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
 it fails. Once all the rules have been processed, if the main subgoal has
 progressed (e.g., if it is distinct from the initial main goal) then the rules
 of this base are processed again. If the main subgoal has not progressed then
@@ -2762,12 +2785,11 @@ command.
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
-%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\
-%{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\
-%These are deprecated syntactic variants for
-%{\tt autorewrite with \ident$_1$ \dots \ident$_n$}
-%and
-%{\tt autorewrite  with \ident$_1$ \dots \ident$_n$ using \tac}.
+
+\item \texttt{autorewrite with {\ident} in {\qualid}}
+
+  Performs all the rewritings in hypothesis {\qualid}.
+
 \end{Variant}
 
 \subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 71db456e9d..eeccbd1191 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -78,7 +78,7 @@ unpublished.
 [Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
-[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
 intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
@@ -125,7 +125,7 @@ Definition FunctionalRelReification_on :=
 
 (** ID_epsilon (constructive version of indefinite description;
     combined with proof-irrelevance, it may be connected to
-    Carlstrøm's type theory with a constructive indefinite description
+    Carlstrøm's type theory with a constructive indefinite description
     operator) *)
 
 Definition ConstructiveIndefiniteDescription_on :=
@@ -133,7 +133,7 @@ Definition ConstructiveIndefiniteDescription_on :=
   (exists x, P x) -> { x:A | P x }.
 
 (** ID_iota (constructive version of definite description; combined
-    with proof-irrelevance, it may be connected to Carlstrøm's and
+    with proof-irrelevance, it may be connected to Carlstrøm's and
     Stenlund's type theory with a constructive definite description
     operator) *)
 
@@ -694,7 +694,7 @@ Qed.
     We adapt the proof to show that constructive definite description
     transports excluded-middle from [Prop] to [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 2be5a0eb64..7b9b09ef55 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -15,7 +15,7 @@
     excluded-middle in [Set], hence it implies a strongly classical
     world. Especially it conflicts with the impredicativity of [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)