diff options
| author | Pierre-Marie Pédrot | 2016-05-09 00:12:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-03 16:51:09 +0200 |
| commit | 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d (patch) | |
| tree | 8134c12bef64decc00490519f2f04e06932355e0 /parsing | |
| parent | 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 (diff) | |
Removing "rename" from the tactic AST.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 6e1731bb2b..36fffd74fa 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -604,9 +604,6 @@ GEXTEND Gram | IDENT "edestruct"; icl = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct(false,true,icl)) - (* Context management *) - | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) - (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) |