diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 10 |
1 files changed, 10 insertions, 0 deletions
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 |