From d9bae9495c689c4a524db165466ead3a42cc51ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Nov 2015 18:24:37 +0100
Subject: [PATCH] Inhabited now lives in Type rather than Prop.

---
 prelude/base.v   | 2 +-
 prelude/finite.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/prelude/base.v b/prelude/base.v
index a94511d4e..36af265f2 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -129,7 +129,7 @@ Arguments decide _ {_}.
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
-Class Inhabited (A : Type) : Prop := populate { _ : A }.
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
 Arguments populate {_} _.
 
 Instance unit_inhabited: Inhabited unit := populate ().
diff --git a/prelude/finite.v b/prelude/finite.v
index 782400116..fed9dd3f7 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -69,7 +69,7 @@ Proof.
 Qed.
 Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A.
 Proof.
-  unfold card. destruct finA as [[|x ?] ??]; simpl; auto with lia.
+  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
   constructor; exact x.
 Qed.
 Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
-- 
GitLab