diff options
| author | notin | 2006-09-01 08:08:22 +0000 |
|---|---|---|
| committer | notin | 2006-09-01 08:08:22 +0000 |
| commit | 03fc5f1d7c143ef65cfc7258e5e158d8405f05a1 (patch) | |
| tree | 4b91ffbdbb43157c7ce8990cce1cee73684d8db6 | |
| parent | 5ea203149ab11b4e837b5a6c95510f67a9e1d784 (diff) | |
Modification du manuel de référence: le flag evar pour cbv n'existe plus.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 1dd534ca29..10e32675b1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -774,9 +774,7 @@ followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded. However, the {\tt delta} flag does not apply to variables bound by a let-in construction whose unfolding is controlled by the {\tt - zeta} flag only. In addition, there is a flag {\tt Evar} to perform -instantiation of existential variables (``?'') when an instantiation -actually exists. + zeta} flag only. The goal may be normalized with two strategies: {\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy @@ -799,7 +797,7 @@ computational expressions (i.e. with few dead code). \begin{Variants} \item {\tt compute} \tacindex{compute} - This tactic is an alias for {\tt cbv beta delta evar iota zeta}. + This tactic is an alias for {\tt cbv beta delta iota zeta}. \item {\tt vm\_compute} \tacindex{vm\_compute} |