diff options
| author | Arnaud Spiwack | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-12-12 16:08:44 +0100 |
| commit | 724797b1f0e7051a52f30ff0cc432db2cc9345ec (patch) | |
| tree | 66038674337785c918a71941d38c19bd62323083 /parsing | |
| parent | a417d138c0a8abc028486c20d59e4f2e82f456ef (diff) | |
Extend the syntax of simpl with a delta flag.
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 324efe53e9..43d787ba59 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -342,7 +342,7 @@ GEXTEND Gram red_tactic: [ [ IDENT "red" -> Red false | IDENT "hnf" -> Hnf - | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po + | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po) | IDENT "cbv"; s = strategy_flag -> Cbv s | IDENT "cbn"; s = strategy_flag -> Cbn s | IDENT "lazy"; s = strategy_flag -> Lazy s @@ -357,7 +357,7 @@ GEXTEND Gram red_expr: [ [ IDENT "red" -> Red false | IDENT "hnf" -> Hnf - | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po + | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po) | IDENT "cbv"; s = strategy_flag -> Cbv s | IDENT "cbn"; s = strategy_flag -> Cbn s | IDENT "lazy"; s = strategy_flag -> Lazy s |