From 64239322013a30cf25b2a1ca4a8f66bff8a7d818 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 13 Nov 2019 11:34:15 +0100
Subject: Register proof_irrelevance

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

diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index e4fbd1c273..4cbbef2757 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -14,6 +14,8 @@ Require Import ProofIrrelevanceFacts.
 
 Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
 
+Register proof_irrelevance as core.proof_irrelevance.
+
 Module PI. Definition proof_irrelevance := proof_irrelevance. End PI.
 
 Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI).
-- 
cgit v1.2.3