From 46648f14678957221d8245bf22c0e5c84a6270a8 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Wed, 4 May 2016 11:50:32 +0200
Subject: [PATCH] remove unneeded, loopy uncurry decision instance

---
 prelude/decidable.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/prelude/decidable.v b/prelude/decidable.v
index 819749a94..76ec22103 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -180,8 +180,6 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
   match p as p return Decision (curry P p) with
   | (x,y) => P_dec x y
   end.
-Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
-  Decision (uncurry P x y) := P_dec (x,y).
 
 Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
-- 
GitLab