diff options
| -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 |