diff --git a/theories/decidable.v b/theories/decidable.v
index 0fa06809d4c5f262f04bf9569702203aa12e59b9..582bd96cafc6387b8bba97f588fbd00d69eaab5d 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -88,6 +88,7 @@ Notation cast_if_not S := (if S then right _ else left _).
 (** We can convert decidable propositions to booleans. *)
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
+Global Arguments bool_decide : simpl never.
 
 Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
 Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.