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 /parsing | |
| 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 '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 |