diff --git a/algebra/excl.v b/algebra/excl.v
index ebdf8f5592fbd461fa209c26642fe631fbc6b9d0..b8ffd8b8db73497608988ee215101727f8c1c1a3 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.