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 /plugins/syntax | |
| parent | 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 (diff) | |
Removing "rename" from the tactic AST.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions