From 8234670f79c16cec502581a29068641b02d43cf5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Jul 2016 14:08:07 +0200
Subject: [PATCH] Qp is inhabited.

---
 prelude/numbers.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prelude/numbers.v b/prelude/numbers.v
index 50d60a0da..2a410297a 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -504,6 +504,8 @@ Infix "+" := Qp_plus : Qp_scope.
 Infix "-" := Qp_minus : 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 ->|].
-- 
GitLab