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 | |
| 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
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 10 |
2 files changed, 16 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 diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 0eab3f7f9c..fe21a876cf 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -204,6 +204,13 @@ GEXTEND Gram | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl ] ] ; + + delta_flag: + [ [ IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl + | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl + ] ] + ; + red_tactic: [ [ IDENT "red" -> Red false | IDENT "hnf" -> Hnf @@ -211,6 +218,9 @@ GEXTEND Gram | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s) | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s) | IDENT "compute" -> compute + | IDENT "compute"; delta = delta_flag -> + let s = [FBeta;FIota;FZeta;delta] in + Cbv (make_red_flag s) | IDENT "vm_compute" -> CbvVm | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl |