diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-06 15:21:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-06 15:32:36 +0200 |
| commit | 3b83b311798f0d06444e1994602e0b531e207ef5 (patch) | |
| tree | 8d41bca774ee92bfa2c9866cc54ef4d7acd5a20c /intf | |
| parent | ce85edee592fef31575e138af2945ce8be74cd07 (diff) | |
Moving the [split] tactic out of the AST.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index eeba560d7..4b4a54a03 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -26,7 +26,6 @@ type lazy_flag = bool (* true = lazy false = eager *) type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) -type split_flag = bool (* true = exists false = split *) type letin_flag = bool (* true = use local def false = use Leibniz *) type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) @@ -141,7 +140,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacRevert of 'nam list (* Trmuctors *) - | TacSplit of evars_flag * split_flag * 'trm bindings list + | TacSplit of evars_flag * 'trm bindings list | TacAnyConstructor of evars_flag * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option | TacConstructor of evars_flag * int or_var * 'trm bindings |