diff options
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 |