From 47755ced3efc7468b00b288dd93f15107683df49 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 16 Apr 2020 15:22:40 +0200
Subject: [PATCH] Add `ProofIrrel ()`

This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.
---
 theories/proof_irrel.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index af527c74..9b2bbc38 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -8,6 +8,8 @@ Instance True_pi: ProofIrrel True.
 Proof. intros [] []; reflexivity. Qed.
 Instance False_pi: ProofIrrel False.
 Proof. intros []. Qed.
+Instance unit_pi: ProofIrrel ().
+Proof. intros [] []; reflexivity. Qed.
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
 Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
-- 
GitLab