diff options
| -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 66f90e18f1..8e1d6d2d8b 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. |