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

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.