From 72094961d9bd7f0f618d30b2b508d8924336d7b4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Jul 2016 10:47:17 +0200
Subject: Program: Move ProofIrrelevance to Subset.v

---
 theories/Program/Subset.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Program/Subset.v')

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c8f37318d1..2a3ec926b2 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,7 @@
 
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
+Require Export ProofIrrelevance.
 
 Local Open Scope program_scope.
 
-- 
cgit v1.2.3