From 3289d1bcc3356eb0f1eb14d3a4a0e201ef927d2e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 09:50:02 +0200
Subject: [PATCH] remove spurious space
---
theories/decidable.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/decidable.v b/theories/decidable.v
index e5572fe5..63c7a376 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -99,7 +99,7 @@ Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
(if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
-Tactic Notation "case_bool_decide" "as" ident (Hd) :=
+Tactic Notation "case_bool_decide" "as" ident(Hd) :=
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
destruct_decide (@bool_decide_reflect P dec) as Hd
--
GitLab