diff --git a/theories/option.v b/theories/option.v
index 78855befa8ba044930e80759011fe64a0c6b3142..eba41dd45904951a73837fa191f63436233c9625 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -22,7 +22,6 @@ Proof. congruence. Qed.
 (** The non dependent elimination principle on the option type. *)
 Definition default {A B} (b : B) (x : option A) (f : A → B)  : B :=
   match x with None => b | Some a => f a end.
-Hint Extern 1000 => simpl (default _ (Some _) _) || simpl (default _ None _).
 
 (** The [from_option] function allows us to get the value out of the option
 type by specifying a default value. *)