diff options
Diffstat (limited to 'doc')
| -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} |