*** empty log message ***

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

1 files changed, 21 insertions, 14 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 297d10035b..886457466a 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -355,6 +355,7 @@ instantiations of the premises of the type of {\term}.
 
 \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}}
 \tacindex{set}
+\tacindex{pose}
 
 This replaces {\term} by {\ident} in the conclusion or in the
 hypotheses of the current goal and adds the new definition {\ident
@@ -368,6 +369,15 @@ replacement only in the conclusion.
   This is equivalent to the above form but applies everywhere in the
   goal (both in conclusion and hypotheses).
 
+\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-}
+  
+  This is equivalent to the above form but applies everywhere in the
+  hypotheses.
+
+\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *}
+  
+  This is equivalent to the default behaviour of {\tt set}.
+
 \item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
   
   This behaves the same but substitutes {\term} not in the goal but in
@@ -383,27 +393,24 @@ to right. A negative occurrence number means an occurrence which
 should not be substituted.
 
 \item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$} \dots
+    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots
     {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
   
-  This is the general form. It substitutes {\term} at occurrences
-  {\num$_1^i$} \dots\ {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One
-  of the {\ident}'s may be the word {\tt Goal}.
+  It substitutes {\term} at occurrences {\num$_1^i$} \dots\
+  {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One of the {\ident}'s
+  may be the word {\tt Goal}.
 
 
 \item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
-\tacindex{pose}
-
-  This is equivalent to the default behavior in {\tt set}.
   
-%  This adds the local definition {\ident} := {\term} to the current
-%  context without performing any replacement in the goal or in the
-%  hypotheses.
+This adds the local definition {\ident} := {\term} to the current
+context without performing any replacement in the goal or in the
+hypotheses.
 
 \item{\tt pose {\term}}
   
-  This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
-  {\ident} is generated by {\Coq}.
+This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
+{\ident} is generated by {\Coq}.
 
 \end{Variants}
 
@@ -624,7 +631,7 @@ tactic \texttt{change}.
 %voir reduction__conv_x : histoires d'univers.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{{\tt cbv} \flag$_1$ \dots\ \flag$_n$, {\tt Lazy} \flag$_1$
+\subsection{{\tt cbv} \flag$_1$ \dots\ \flag$_n$, {\tt lazy} \flag$_1$
 \dots\ \flag$_n$ {\rm and} {\tt compute}}
 \tacindex{cbv}\tacindex{lazy}
 
@@ -1796,7 +1803,7 @@ Abort.
 \SeeAlso~\ref{inversion-examples} for detailed examples
 
 \subsection{\tt Derive Inversion {\ident} with
-  $forall (\vec{x}:\vec{T}), I~\vec{t}$ Sort \sort}
+  ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort}
 \label{Derive-Inversion}
 \comindex{Derive Inversion}
 \index[tactic]{Derive Inversion@{\tt Derive Inversion}}