From 782731f697f4a8d6952ab826eaef37e60be21e8e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 8 Aug 2016 19:12:09 +0200
Subject: [PATCH] Inhabited instance for any Empty instance.

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

diff --git a/theories/base.v b/theories/base.v
index b046cf8e..370621e1 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+
 Class Top A := top : A.
 Notation "⊤" := top : C_scope.
 
-- 
GitLab