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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 8008cac00..16ea80f90 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -400,7 +400,7 @@ misc/deps-order.log: } > "$@" # Sort universes for the whole standard library -EXPECTED_UNIVERSES := 3 +EXPECTED_UNIVERSES := 4 universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" |