diff --git a/theories/decidable.v b/theories/decidable.v
index e5572fe50daed3a0ae30a76e7bf1dfe3a12c3c49..63c7a376d053f47e26ae43622f9fac333b290784 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