MAJ Intro + divers

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

1 files changed, 38 insertions, 35 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 05ba99764..1275134af 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -189,30 +189,35 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which
 \subsection{\tt Intro}
 \tacindex{Intro}
 \label{Intro}
-This tactic applies to a goal which is a product. It implements the
+This tactic applies to a goal which is either a product or starts with
+a let binder. If the goal is a product, the tactic implements the
 ``Lam''\index{Typing rules!Lam} rule given in section
-\ref{Typed-terms}.  Actually, only one subgoal will be generated since the
-other one can be automatically checked.
-
-If the current goal is a dependent product {\tt (x:T)U} and
-{\tt x} is a name that does not exist in the current context, then
-{\tt Intro} puts {\tt x:T} in the local context. Otherwise, it puts
-{\tt x}{\it n}{\tt :T} where {\it n} is such that {\tt x}{\it n} is a
-fresh name. The new subgoal is {\tt U}. If the {\tt x} has been
-renamed {\tt x}{\it n} then it is replaced by {\tt x}{\it n} in {\tt
-U}.
-
-If the goal is a non dependent product T -> U, then it
-puts in the local context either {\tt H}{\it n}{\tt :T} 
-(if {\tt T} is {\tt Set} or {\tt Prop}) or {\tt X}{\it n}{\tt :T} (if
-the type of {\tt T} is {\tt Type}) or {\tt l}{\it n}{\tt :T} with {\it l}
-the first letter of the type of x. {\it n} is such that {\tt H}{\it
-  n} or {\tt X}{\it n} {\tt l}{\it n} or are fresh identifiers.
-In both cases the new subgoal is {\tt U}. 
-
-If the goal is not a product, the tactic {\tt Intro} applies the tactic
-{\tt Red} until the tactic {\tt Intro} can be applied or the goal is not
-reducible.
+\ref{Typed-terms}\footnote{Actually, only the second subgoal will be
+generated since the other one can be automatically checked.}.  If the
+goal starts with a let binder then the tactic implements a mix of the
+``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}.
+
+If the current goal is a dependent product {\tt (x:T)U} (resp {\tt
+[x:=t]U}) then {\tt Intro} puts {\tt x:T} (resp {\tt x:=t}) in the
+local context.
+% Obsolete (quantified names already avoid hypotheses names):
+% Otherwise, it puts
+% {\tt x}{\it n}{\tt :T} where {\it n} is such that {\tt x}{\it n} is a
+%fresh name.
+The new subgoal is {\tt U}.
+% If the {\tt x} has been renamed {\tt x}{\it n} then it is replaced 
+% by {\tt x}{\it n} in {\tt U}. 
+
+If the goal is a non dependent product T -> U, then it puts in the
+local context either {\tt H}{\it n}{\tt :T} (if {\tt T} is {\tt Set}
+or {\tt Prop}) or {\tt X}{\it n}{\tt :T} (if the type of {\tt T} is
+{\tt Type}) {\it n} is such that {\tt H}{\it n} or {\tt X}{\it n}
+{\tt l}{\it n} or are fresh identifiers.  In both cases the new
+subgoal is {\tt U}.
+
+If the goal is neither a product nor starting with a let definition,
+the tactic {\tt Intro} applies the tactic {\tt Red} until the tactic
+{\tt Intro} can be applied or the goal is not reducible.
 
 \begin{ErrMsgs}
 \item \errindex{No product even after head-reduction}
@@ -230,10 +235,9 @@ reducible.
 
   \ErrMsg \errindex{name {\ident} is already bound }
 
-  \Rem {\tt Intro} doesn't check the whole current context. Actually,
-  identifiers declared or defined in required modules can be used as
-  {\ident} and, in this case, the old {\ident} of the module is no
-  more reachable.
+  \Rem If a name used by {\tt Intro} hides the base name of a global
+  constant then the latter can still be referred to by a qualified name
+  (see \ref{LongNames}).
 
 \item {\tt Intros \ident$_1$ \dots\ \ident$_n$} \\ 
   Is equivalent to the composed tactic {\tt Intro \ident$_1$; \dots\ ; Intro
@@ -241,7 +245,7 @@ reducible.
 More generally, the \texttt{Intros} tactic takes a pattern as argument
   in order to introduce names for components of an inductive
   definition or to clear introduced hypotheses; 
-  it will be explained in~\ref{Intros-pattern}.
+  This is explained in~\ref{Intros-pattern}.
 
 \item {\tt Intros until {\ident}}
   \tacindex{Intros until}\\ 
@@ -394,8 +398,7 @@ of the {\ident}'s may be the word {\tt Goal}.
 \subsection{\tt Assert {\ident} : {\form}}\tacindex{Assert}
 This tactic applies to any goal. {\tt Assert H : U} adds a new
 hypothesis of name \texttt{H} asserting \texttt{U} to the current goal
-and opens a new subgoal \texttt{U}. (This corresponds to the cut rule of
-sequent calculus.) The subgoal {\texttt U} comes first in the list of
+and opens a new subgoal \texttt{U}\footnote{This corresponds to the cut rule of sequent calculus.}. The subgoal {\texttt U} comes first in the list of
 subgoals remaining to prove.
 
 \begin{ErrMsgs}
@@ -406,8 +409,8 @@ subgoals remaining to prove.
 
 \begin{Variants}
 \item{\tt Assert {\form}}\\
-  This behaves as {\tt Assert {\ident} : {\form}} but automatically
-  generating a fresh name {\ident} to refer to the asserted hypothesis.
+  This behaves as {\tt Assert {\ident} : {\form}} but {\ident} is
+  generated by {\Coq}.
 
 \item {\tt Cut {\form}}\tacindex{Cut} \\
   This tactic applies to any goal. It implements the non dependent
@@ -499,7 +502,7 @@ that \U\ is well-formed and that \T\ and \U\ are
 convertible.
 
 \begin{ErrMsgs}
-\item \errindex{convert-concl rule passed non-converting term}
+\item \errindex{Not convertible}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -575,7 +578,7 @@ tactic \texttt{Change}.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{{\tt Cbv} \flag$_1$ \dots\ \flag$_n$, {\tt Lazy} \flag$_1$
-\dots\ \flag$_n$ and {\tt Compute}}
+\dots\ \flag$_n$ {\rm and} {\tt Compute}}
 \tacindex{Cbv}\tacindex{Lazy}
 
 These parameterized reduction tactics apply to any goal and perform
@@ -908,7 +911,7 @@ of the goal, and similarly as {\tt NewInduction \ident}, when
 
 \subsection{\tt NewDestruct \term}\tacindex{Destruct}\tacindex{NewDestruct}
 The tactic {\tt NewDestruct} is used to perform case analysis without
-recursion. It behaves as {\tt NewInduction \term} except that no
+recursion. Its behaviour is similar to {\tt NewInduction \term} except that no
 induction hypotheses is generated.  It applies to any goal and the
 type of {\term} must be inductively defined.
 {\tt NewDestruct} works also when {\term} is an identifier denoting a