diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /tactics/inv.ml | |
| 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/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index ee875ce27..36affb541 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -308,9 +308,11 @@ let projectAndApply thin id eqname names depids = | _ -> tac id end in - let deq_trailer id _ neqns = + let deq_trailer id clear_flag _ neqns = tclTHENLIST - [(if not (List.is_empty names) then clear [id] else tclIDTAC); + [apply_clear_request clear_flag + (not (List.is_empty names) || use_clear_hyp_by_default ()) + (mkVar id); (tclMAP_i neqns (fun idopt -> tclTRY (tclTHEN (intro_move idopt MoveLast) @@ -325,7 +327,7 @@ let projectAndApply thin id eqname names depids = (* and apply a trailer which again try to substitute *) (fun id -> dEqThen false (deq_trailer id) - (Some (ElimOnConstr (mkVar id,NoBindings)))) + (Some (None,ElimOnConstr (mkVar id,NoBindings)))) id let nLastDecls i tac = |