diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-17 18:51:20 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-17 18:51:20 +0000 |
commit | 195dc9ae3928a62e58977d8a2582660951d17b9c (patch) | |
tree | f62f4c43fa9af39eafb262c0f3826f26565c9959 /theories/Init/Tactics.v | |
parent | 68939c0d9791564db4876eded273ad53cf107309 (diff) |
New tactic "clear dependent", for the moment in ltac in Init/Tactics
for the moment, only one hypothesis name is accepted after clear
dependent (seems to be also the case for generalize dependent).
Btw, added an alternative name "revert dependent" for "generalize
dependent", since this tactics remove hypothesis from the context.
To be documentated later...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Tactics.v')
-rw-r--r-- | theories/Init/Tactics.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 66f90e18f..8e1d6d2d8 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -207,3 +207,20 @@ Tactic Notation "decide" constr(lemma) "with" constr(H) := | ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H | _ => apply (decide_left lemma H); try_to_merge_hyps H end. + +(** Clear an hypothesis and its dependencies *) + +Tactic Notation "clear" "dependent" ident(h) := + let rec depclear h := + clear h || + match goal with + | H : context [ h ] |- _ => depclear H; depclear h + end || + fail "hypothesis to clear is used in the conclusion (maybe indirectly)" + in depclear h. + +(** Revert an hypothesis and its dependencies : + this is actually generalize dependent... *) + +Tactic Notation "revert" "dependent" ident(h) := + generalize dependent h. |