diff options
| author | jforest | 2007-04-05 16:53:46 +0000 |
|---|---|---|
| committer | jforest | 2007-04-05 16:53:46 +0000 |
| commit | 548fd57a9910a1622348c4a6f6f44f8d8a262bb1 (patch) | |
| tree | b1a3b39ab080a6d0e1806214c161309c9d1a29a0 /doc | |
| parent | 443e5f39a15752541e54bf70058b9da1aa27c33d (diff) | |
Mise en place d'un rafinement de compute.
On peut desormais utiliser:
compute delta [f g ...] pour cbv beta iota zera delta [f g ...] et
compute delta - [f g ...] pour cbv beta iota zera delta - [f g ...]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9749 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d2753371b8..8331defbb5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -873,6 +873,12 @@ computational expressions (i.e. with few dead code). This tactic is an alias for {\tt cbv beta delta iota zeta}. +\item {\tt compute delta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt compute delta -[\qualid$_1$\ldots\qualid$_k$]}) \tacindex{compute} + + This tactic is an alias for {\tt cbv beta delta iota zeta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt cbv beta delta iota zeta -[\qualid$_1$\ldots\qualid$_k$]}) . + + This tactic is an alias for {\tt cbv beta delta iota zeta}. + \item {\tt vm\_compute} \tacindex{vm\_compute} This tactic evaluates the goal using the optimized call-by-value |