aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/UniversesFacts.v
AgeCommit message (Expand)Author
2012-11-15Isolating the ingredients of the proof of Prop<>Type (r15973). Seeingherbelin
2012-11-15Added a proof that Prop<>Type, for arbitrary fixed Type.herbelin