Quelques pr�cisions sur la convertibilit� et les tactiques Cbv/Lazy

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

2 files changed, 7 insertions, 3 deletions

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 391bcf27c..3dfe40617 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -375,7 +375,7 @@ $$\WTEGRED{[x:=u]t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$
 \label{convertibility}
 \index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}
 
-Let us write $\WTEGRED{t}{\triangleright}{u}$ for the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
+Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
 
 We say that two terms $t_1$ and $t_2$ are {\em convertible} (or {\em
   equivalent)} in the environment $E$ and context $\Gamma$ iff there exists a term $u$ such that $\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u}$
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index afefa3204..28307b4f3 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -605,14 +605,18 @@ $\iota$ (reduction of {\tt Cases}, {\tt Fix} and {\tt
 CoFix} expressions) and $\zeta$ (removal of local definitions), every flag is one of {\tt Beta}, {\tt Delta},
 {\tt Iota}, {\tt Zeta}, {\tt [\qualid$_1$\ldots\qualid$_k$]} and 
 {\tt -[\qualid$_1$\ldots\qualid$_k$]}.
-The last two flags give the list of
-constants to unfold, or the list of constants not to unfold. These two
+The last two flags give the list of constants to unfold, or the list
+of constants not to unfold. These two
 flags can occur only after the {\tt Delta} flag. 
+For these tactics, the {\tt Delta} flag does not apply to
+variables bound by a let-in construction of which the unfolding is
+controlled by the {\tt Zeta} flag only.
 In addition, there is a flag {\tt Evar} to perform instantiation of exitential variables (``?'') when an instantiation actually exists.
 The goal may be
 normalized with two strategies: {\em lazy} ({\tt Lazy} tactic), or
 {\em call-by-value} ({\tt Cbv} tactic).
 
+Notice that, for these tactics, the {\tt Delta} flag without rest should be understood as unfolding all
 The lazy strategy is a call-by-need strategy, with sharing of
 reductions: the arguments of a function call are partially evaluated
 only when necessary, but if an argument is used several times, it is