From e8075845be8582d542cd9fec0440727c0f387167 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Nov 2016 10:19:20 +0100
Subject: [PATCH] Decidable equality of Qp.

---
 theories/numbers.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 46cc4179..38f5a862 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -517,13 +517,18 @@ Infix "-" := Qp_minus : Qp_scope.
 Infix "*" := Qp_mult : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
 
-Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
-
 Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
 Proof.
   split; [by intros ->|].
   destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
 Qed.
+
+Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
+Instance Qp_eq_dec : EqDecision Qp.
+Proof.
+ refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq.
+Defined.
+
 Instance Qp_plus_assoc : Assoc (=) Qp_plus.
 Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
 Instance Qp_plus_comm : Comm (=) Qp_plus.
-- 
GitLab