From dbb8d7c9c89d22bd74775b7bbe707f4a9947c41d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 May 2016 21:59:10 +0200
Subject: [PATCH] Functions are inhabited.

---
 prelude/base.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prelude/base.v b/prelude/base.v
index 72d51f9be..ff635a1a3 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -306,6 +306,9 @@ Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
 Notation "(∘ f )" := (λ g, compose g f) (only parsing) : C_scope.
 
+Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
+  populate (λ _, inhabitant).
+
 (** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
 applied. *)
 Arguments id _ _ /.
-- 
GitLab