From 718ca5be1420dc5ad9f16e763330afd6ced0d449 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Feb 2020 08:48:44 +0100
Subject: [PATCH] `Prop` is inhabited.

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

diff --git a/theories/base.v b/theories/base.v
index dfedf6f0..30feccb2 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -413,6 +413,8 @@ Class TotalOrder {A} (R : relation A) : Prop := {
 }.
 
 (** * Logic *)
+Instance prop_inhabited : Inhabited Prop := populate True.
+
 Notation "(∧)" := and (only parsing) : stdpp_scope.
 Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
 Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.
-- 
GitLab