coq/test-suite/unit-tests/lib, branch master The formal proof system Make prvect tail recursive (fix #9355) 2019-01-22T13:09:34+00:00 Gaëtan Gilbert 2019-01-19T22:16:06+00:00 4baa950b79589c6617770b5612bd082fde9c9255 Using a unit test as it's way faster than messing with universes. You can test with universes by ~~~coq Set Universe Polymorphism. Definition x1@{i} := True. Definition x2 := x1 -> x1. Definition x3 := x2 -> x2. Definition x4 := x3 -> x3. Definition x5 := x4 -> x4. Definition x6 := x5 -> x5. Definition x7 := x6 -> x6. Definition x8 := x7 -> x7. Definition x9 := x8 -> x8. Definition x10 := x9 -> x9. Definition x11 := x10 -> x10. Definition x12 := x11 -> x11. Definition x13 := x12 -> x12. Definition x14 := x13 -> x13. Definition x15 := x14 -> x14. Definition x16 := x15 -> x15. Definition x17 := x16 -> x16. Definition x18 := x17 -> x17. Definition x19 := x18 -> x18. About x19. (* 262144 universes *) ~~~ Note on my machine `About x18.` did not overflow even before this commit. 
Using a unit test as it's way faster than messing with universes.

You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.

About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.