diff --git a/tests/tactics.ref b/tests/tactics.ref
new file mode 100644
index 0000000000000000000000000000000000000000..df107d33b08b5d6b7603b8d4da31cbd82ce93e2e
--- /dev/null
+++ b/tests/tactics.ref
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_or !" failed.
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_and !" failed.
+Failed to progress.
diff --git a/tests/tactics.v b/tests/tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..a606dbce49240e9ab1c77b09021650da74a93531
--- /dev/null
+++ b/tests/tactics.v
@@ -0,0 +1,50 @@
+From stdpp Require Import tactics.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
+  (P1 → P) →
+  (P2 → P) →
+  (P3 → P) →
+  (P4 → P) →
+  P.
+Proof.
+  intros * HH X1 X2 X3 X4.
+  destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
+Qed.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  P1 ∨ P2 →
+  P3 ∨ P4 →
+  (P1 → P3 → P) →
+  (P1 → P4 → P) →
+  (P2 → P3 → P) →
+  (P2 → P4 → P) →
+  P.
+Proof.
+  intros * HH1 HH2 X1 X2 X3 X4.
+  destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
+Qed.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  id (P1 ∨ P2) →
+  id (P3 ∨ P4) →
+  (P1 → P3 → P) →
+  (P1 → P4 → P) →
+  (P2 → P3 → P) →
+  (P2 → P4 → P) →
+  P.
+Proof.
+  intros * HH1 HH2 X1 X2 X3 X4.
+  Fail progress destruct_or?.
+  Fail progress destruct_or!.
+  destruct_or! HH1; destruct_or! HH2;
+  [ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
+Qed.
+
+Goal forall P1 P2 P3 P4,
+  P1 ∧ (Is_true (P2 && P3)) ∧ P4 →
+  P1 ∧ P2 ∧ P3.
+Proof.
+  intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
+  destruct_and?. Fail destruct_and!. assumption.
+Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index 2203968c710220efecb758abb213484cb8391bae..4fa8bb94d78117e3b13c1d81a81339187ebde5ca 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -91,7 +91,17 @@ Tactic Notation "etrans" := etransitivity.
   conjunction.
 
 Note that [split_and] differs from [split] by only splitting conjunctions. The
-[split] tactic splits any inductive with one constructor. *)
+[split] tactic splits any inductive with one constructor.
+
+
+- [destruct_and? H] : destruct assumption [H] repeatedly (perhaps zero times)
+  while it is of the shape [_ ∧ _].
+- [destruct_and! H] : works similarly, but at least one destruct should succeed.
+  In order to do so, it will head normalize the goal first to possibly expose a
+  conjunction.
+- [destruct_and?] iterates [destruct_or? H] on every matching assumption [H].
+- [destruct_and!] works similarly, but at least one destruct should succeed.
+*)
 Tactic Notation "split_and" :=
   match goal with
   | |- _ ∧ _ => split
@@ -100,14 +110,56 @@ Tactic Notation "split_and" :=
 Tactic Notation "split_and" "?" := repeat split_and.
 Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
 
+Ltac destruct_and_go H :=
+  try lazymatch type of H with
+  | False => destruct H
+  | _ ∧ _ =>
+    let H1 := fresh in
+    let H2 := fresh in
+    destruct H as [ H1 H2 ];
+    destruct_and_go H1; destruct_and_go H2
+  | Is_true (bool_decide _) =>
+    apply (bool_decide_unpack _) in H;
+    destruct_and_go H
+  | Is_true (_ && _) =>
+    apply andb_True in H;
+    destruct_and_go H
+  end.
+
+Tactic Notation "destruct_and" "?" ident(H) :=
+  destruct_and_go H.
+Tactic Notation "destruct_and" "!" ident(H) :=
+  hnf in H; progress (destruct_and? H).
+
 Tactic Notation "destruct_and" "?" :=
-  repeat match goal with
-  | H : False |- _ => destruct H
-  | H : _ ∧ _ |- _ => destruct H
-  | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
-  | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
+  repeat match goal with H : _ |- _ => progress (destruct_and? H) end.
+Tactic Notation "destruct_and" "!" :=
+  progress destruct_and?.
+
+(** Tactics for splitting disjunctions in an assumption:
+
+- [destruct_or? H] : destruct the assumption [H] repeatedly (perhaps zero times)
+  while it is of the shape [_ ∨ _].
+- [destruct_or! H] : works similarly, but at least one destruct should succeed.
+  In order to do so, it will head normalize the goal first to possibly
+  expose a disjunction.
+- [destruct_or?] iterates [destruct_or? H] on every matching assumption [H].
+- [destruct_or!] works similarly, but at least one destruct should succeed.
+*)
+Tactic Notation "destruct_or" "?" ident(H) :=
+  repeat match type of H with
+  | True => clear H
+  | _ ∨ _ => destruct H as [H|H]
+  | Is_true (bool_decide _) => apply (bool_decide_unpack _) in H
+  | Is_true (_ || _) => apply orb_True in H; destruct H as [H|H]
   end.
-Tactic Notation "destruct_and" "!" := progress (destruct_and?).
+Tactic Notation "destruct_or" "!" ident(H) := hnf in H; progress (destruct_or? H).
+
+Tactic Notation "destruct_or" "?" :=
+  repeat match goal with H : _ |- _ => progress (destruct_or? H) end.
+Tactic Notation "destruct_or" "!" :=
+  progress destruct_or?.
+
 
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used