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 /intf | |
| parent | 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 (diff) | |
Removing "rename" from the tactic AST.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e1d4809609..379dd59d39 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -156,9 +156,6 @@ type 'a gen_atomic_tactic_expr = | TacInductionDestruct of rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list - (* Context management *) - | TacRename of ('nam *'nam) list - (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr |