Documentation v8 de 'set (id:=t) in ...'

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

1 files changed, 43 insertions, 18 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 25e0f7aed..cb4abb22e 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -383,10 +383,6 @@ second-order pattern-matching problem into a first-order one.
 \tacindex{set}
 \tacindex{pose}}
 
-\Warning V8 updating to do
-
-\medskip
-
 This replaces {\term} by {\ident} in the conclusion or in the
 hypotheses of the current goal and adds the new definition {\ident
 {\tt :=} \term} to the local context. The default is to make this
@@ -394,41 +390,70 @@ replacement only in the conclusion.
 
 \begin{Variants}
 
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}
+\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\
+  {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\
   
-  This is equivalent to the above form but applies everywhere in the
-  goal (both in conclusion and hypotheses).
+  This behaves as above but substitutes {\term}
+  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.
+  This behaves the same but substitutes {\term} in
+  the hypotheses only (not in the conclusion).
 
 \item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *}
   
-  This is equivalent to the default behavior of {\tt set}.
+  This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt
+  )}, i.e. it substitutes {\term} in the conclusion only.
 
 \item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
   
-  This behaves the same but substitutes {\term} not in the goal but in
+  This behaves the same but substitutes {\term} only in
   the hypothesis named {\ident$_1$}.
   
 \item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
     {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$}
 
-This notation allows to specify which occurrences of the hypothesis
-named {\ident$_1$} (or the goal if {\ident$_1$} is the word {\tt
-  Goal}) should be substituted. The occurrences are numbered from left
-to right. A negative occurrence number means an occurrence which
-should not be substituted.
+This notation allows to specify which occurrences of {\term} have to
+be substituted in the hypothesis named {\ident$_1$}. The occurrences
+are numbered from left to right and are meaningful on a pure
+expression using no implicit argument, notation or coercion. A
+negative occurrence number means an occurrence which should not be
+substituted. As an exception of the left-to-right order, the
+occurrences in the {\tt return} subexpression of a {\tt match} are
+considered {\em before} the occurrences in the matched term.
+
+For expressions using notations, or hiding implicit arguments or
+coercions, it is recommended to make explicit all occurrences in 
+order by using {\tt Set Printing All} (see
+section~\ref{SetPrintingAll}).
+
+\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at}
+      {\num$_1$} \dots\ {\num$_n$}
+  
+This allows to specify which occurrences of the conclusion are concerned.
 
 \item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
     {\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$}
   
   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}.
+  {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is
+  optional.
+
+\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
+    {\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$}
+    {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$}
+
+  This is the more general form which combines all the previous
+  possibilities.
+
+\item {\tt set } {\term}
+
+  This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident}
+    is generated by {\Coq}. This variant is available for the 
+    forms with {\tt in} too.
 
 \item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}