From c24ab2eebf575b9ea789456b53c303e7cad6c9b0 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.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index 56b1706a..df8c21a2 100644
--- a/theories/numbers.v
+++ b/theories/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