diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 12:40:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 13:24:45 +0100 |
| commit | 293222e49ff81bc1299b3822d2a8c526ca803307 (patch) | |
| tree | fff87b81ee563870658be00b3686e70d3262cf59 /intf | |
| parent | ae3bbff3ca2564fe24bdf3dd517c82807eae9151 (diff) | |
Moving the "exists" tactic to TACTIC EXTEND.
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 3f1d0fd76..dae960e0e 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -163,9 +163,6 @@ type 'a gen_atomic_tactic_expr = | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list - (* Trmuctors *) - | TacSplit of evars_flag * 'trm bindings list - (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr |