From 96e5b76236e22e3e481e4bae0f80f8ab4fb864bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 16:19:34 +0100
Subject: [PATCH] Destructor for dec_agree.

---
 algebra/dec_agree.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 753bc8073..901fe1439 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -10,6 +10,8 @@ Inductive dec_agree (A : Type) : Type :=
   | DecAgreeBot : dec_agree A.
 Arguments DecAgree {_} _.
 Arguments DecAgreeBot {_}.
+Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
+  match x with DecAgree a => Some a | _ => None end.
 
 Section dec_agree.
 Context {A : Type} `{∀ x y : A, Decision (x = y)}.
-- 
GitLab