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 /tactics/equality.mli | |
| 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 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 82e30b9401..2993c8d3a4 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -64,7 +64,7 @@ type delayed_open_constr_with_bindings = env -> evar_map -> evar_map * constr with_bindings val general_multi_multi_rewrite : - evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> + evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic @@ -78,14 +78,14 @@ val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic val inj : intro_pattern_expr Loc.located list option -> evars_flag -> - constr with_bindings -> unit Proofview.tactic + clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : intro_pattern_expr Loc.located list option -> evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic -val injHyp : Id.t -> unit Proofview.tactic +val injHyp : clear_flag -> Id.t -> unit Proofview.tactic val injConcl : unit Proofview.tactic val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic +val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) |