From bf59ec9e937fe555e02d76f666c76454d243aebb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 15:36:14 +0200
Subject: [PATCH] Destructors for csum.

---
 algebra/csum.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/algebra/csum.v b/algebra/csum.v
index d8a4d66ad..211029607 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -15,6 +15,11 @@ Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
 Arguments CsumBot {_ _}.
 
+Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
+  match x with Cinl a => Some a | _ => None end.
+Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
+  match x with Cinr b => Some b | _ => None end.
+
 Section cofe.
 Context {A B : cofeT}.
 Implicit Types a : A.
-- 
GitLab