diff --git a/theories/option.v b/theories/option.v
index ed02330a6d8b93ab8b504a7d7f6671ace5e18f69..8a6f893ca70d5e7d728acdd76a96c45406ca576a 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -68,8 +68,6 @@ Definition Some_dec {A} (x : option A) : { a | x = Some a } + { x = None } :=
   | Some a => inleft (a ↾ eq_refl _)
   | None => inright eq_refl
   end.
-Instance None_dec {A} (x : option A) : Decision (x = None) :=
-  match x with Some x => right (Some_ne_None x) | None => left eq_refl end.
 
 Lemma eq_None_not_Some {A} (x : option A) : x = None ↔ ¬is_Some x.
 Proof. destruct x; unfold is_Some; naive_solver. Qed.