Add Arguments bool_decide : simpl never

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.