diff options
| author | Hugo Herbelin | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /intf | |
| parent | 8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (diff) | |
Experimentally adding an option for automatically erasing an
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).
Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 4174de1230..0c5eed7144 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -25,14 +25,18 @@ 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 letin_flag = bool (* true = use local def false = use Leibniz *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) -type 'a induction_arg = +type 'a core_induction_arg = | ElimOnConstr of 'a | ElimOnIdent of Id.t located | ElimOnAnonHyp of int +type 'a induction_arg = + clear_flag * 'a core_induction_arg + type inversion_kind = | SimpleInversion | FullInversion @@ -62,6 +66,8 @@ type ('constr,'id) induction_clause_list = * 'constr with_bindings option (* using ... *) * 'id clause_expr option (* in ... *) +type 'a with_bindings_arg = clear_flag * 'a with_bindings + type multi = | Precisely of int | UpTo of int @@ -108,10 +114,10 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacIntrosUntil of quantified_hypothesis | TacIntroMove of Id.t option * 'nam move_location | TacExact of 'trm - | TacApply of advanced_flag * evars_flag * 'trm with_bindings list * - ('nam * intro_pattern_expr located option) option - | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option - | TacCase of evars_flag * 'trm with_bindings + | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * + (clear_flag * 'nam * intro_pattern_expr located option) option + | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option + | TacCase of evars_flag * 'trm with_bindings_arg | TacFix of Id.t option * int | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacCofix of Id.t option @@ -157,7 +163,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'trm with_bindings) list * 'nam clause_expr * + (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis |