From c2725b246325fc8662a576d946fd8aa4b6d011ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 13:08:29 +0100
Subject: [PATCH] Remove weird type class constraint in excl.

---
 algebra/excl.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/excl.v b/algebra/excl.v
index ebdf8f559..b8ffd8b8d 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -22,7 +22,7 @@ Inductive excl_equiv : Equiv (excl A) :=
   | ExclUnit_equiv : ExclUnit ≡ ExclUnit
   | ExclBot_equiv : ExclBot ≡ ExclBot.
 Existing Instance excl_equiv.
-Inductive excl_dist `{Dist A} : Dist (excl A) :=
+Inductive excl_dist : Dist (excl A) :=
   | Excl_dist (x y : A) n : x ≡{n}≡ y → Excl x ≡{n}≡ Excl y
   | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
   | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
-- 
GitLab