diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-18 03:40:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-18 03:40:42 +0000 |
| commit | 1c25f8bc8d926e85667d321555775200ddfd17d2 (patch) | |
| tree | 2e596fd8ff73ac1d192c0a77701408abbe631a58 /lib | |
| parent | 873d23c66aa447e5cc9ed3b782956ae0d268589b (diff) | |
Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)
universes. As it uses eq_rect on Type(2), the arguments of eq_rect
has to be in Type(3) and compiling the standard library now needs one
more universe! If needed, we could avoid this by inlining the
definition of (eq_rect Type2) in Hurkens.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions