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

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"