From 9e62dc0d0ce67af1375e1572b9d5f7bebfbce792 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Mar 2002 17:18:42 +0000
Subject: 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
---
 doc/RefMan-tac.tex | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc/RefMan-tac.tex')

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index afefa32046..28307b4f35 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
-- 
cgit v1.2.3

