From ada321d100130c4f59d0ea4c47e9a9390a47bd7a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jun 2016 01:16:03 +0200
Subject: [PATCH] Remove useless type class instance.

---
 algebra/dec_agree.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 843c10767..068ec54b1 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -18,7 +18,6 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Instance dec_agree_equiv : Equiv (dec_agree A) := equivL.
 Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
-- 
GitLab