From 364f5410c1f6d3f033038aa17bb797fd277c5b3c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 23 Nov 2014 14:55:38 +0100
Subject: [PATCH] Remove duplicate None decider.

---
 theories/option.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index ed02330a..8a6f893c 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.
-- 
GitLab