Bool: shorter and more systematic proofs + an iff lemma about eqb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index a92d9b1ef..58827eefb 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -88,6 +88,14 @@ Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
 Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
   try intros until n; destruct n as []_eqn:H.
 
+(** Break every hypothesis of a certain type *)
+
+Ltac destruct_all t :=
+ match goal with
+  | x : t |- _ => destruct x; destruct_all t
+  | _ => idtac
+ end.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.