From 82b3e17df877a10ba05ee86e715c487525e9cd18 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Jun 2019 17:11:28 +0200
Subject: [PATCH] more auto
---
theories/decidable.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/decidable.v b/theories/decidable.v
index ddb90db6..e9d3af21 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -126,7 +126,7 @@ Lemma bool_decide_false_2 P `{!Decision P}: bool_decide P = false → ¬P.
Proof.
intros Heq HP. assert (HP': bool_decide P).
{ apply bool_decide_spec. assumption. }
- destruct (bool_decide P). discriminate. contradiction.
+ case_bool_decide; auto || discriminate.
Qed.
(** * Decidable Sigma types *)
--
GitLab