aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-08 10:47:17 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-08 10:47:17 +0200
commit72094961d9bd7f0f618d30b2b508d8924336d7b4 (patch)
tree380ab757e73d569483272797fa881c55b5818a28 /library
parent21be7a5dba2fdfa40fd7b4a3d94610947d202bb7 (diff)
Program: Move ProofIrrelevance to Subset.v
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions