From 195dc9ae3928a62e58977d8a2582660951d17b9c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 17 Jun 2010 18:51:20 +0000
Subject: 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
---
 theories/Init/Tactics.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

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.
-- 
cgit v1.2.3