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/extratactics.ml4 | |
| 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/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8cf1e531dd..a7d95c5e89 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -65,8 +65,8 @@ TACTIC EXTEND replace_term END let induction_arg_of_quantified_hyp = function - | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Loc.ghost,id) + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a @@ -74,7 +74,7 @@ let induction_arg_of_quantified_hyp = function let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (ElimOnConstr c.it)) + c.sigma (Some (None,ElimOnConstr c.it)) TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> |