From 39d73ee8df7d8f0095128dd3b02ca7ae0c5efe37 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Dec 2014 00:42:16 +0100
Subject: [PATCH] Misc option stuff.

---
 theories/option.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/option.v b/theories/option.v
index 8a6f893c..182b5a16 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -86,7 +86,7 @@ Proof.
   match x, y with
   | Some a, Some b => cast_if (decide (a = b))
   | None, None => left _ | _, _ => right _
-  end; abstract congruence.
+  end; clear dec; abstract congruence.
 Defined.
 
 (** * Monadic operations *)
@@ -159,6 +159,8 @@ Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
   match xy with inl x => Some x | _ => None end.
 Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
   match xy with inr y => Some y | _ => None end.
+Instance maybe_Some {A} : Maybe (@Some A) := id.
+Arguments maybe_Some _ !_ /.
 
 (** * Union, intersection and difference *)
 Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
-- 
GitLab