From 8fc099dcc16a3da2ce5cc7027598a99af757b051 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Mar 2017 10:44:26 +0100
Subject: [PATCH] Add conditional `done` tactic.

---
 theories/tactics.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/tactics.v b/theories/tactics.v
index 250f8651..1c07fd48 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.
-- 
GitLab