diff --git a/theories/tactics.v b/theories/tactics.v
index 250f8651b6aac121974be848279543453e815b7d..1c07fd4833225a58066687932706518d4b85266f 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -72,6 +72,12 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
+Ltac done_if b :=
+  match b with
+  | true => done
+  | false => idtac
+  end.
+
 (** Aliases for trans and etrans that are easier to type *)
 Tactic Notation "trans" constr(A) := transitivity A.
 Tactic Notation "etrans" := etransitivity.