| Age | Commit message (Expand) | Author |
|---|---|---|
| 2019-05-10 | [api] Remove 8.10 deprecations. | Emilio Jesus Gallego Arias |
| 2019-03-14 | Add a non-cumulative impredicative universe SProp. | Gaëtan Gilbert |
| 2019-03-14 | Make Sorts.t private | Gaëtan Gilbert |
| 2018-12-06 | Revise API for global universes. | Gaëtan Gilbert |
| 2018-12-06 | Fix race condition triggered by fresh universe generation | Maxime Dénès |
| 2018-10-18 | [universes] deprecate constr_of_global | Matthieu Sozeau |
| 2018-10-16 | UnivGen.extend_context -> Univ.extend_in_context_set | Gaëtan Gilbert |
| 2018-10-16 | Clean UnivGen.fresh_instance API | Gaëtan Gilbert |
| 2018-10-16 | Simplify UnivGen.type_of_reference | Gaëtan Gilbert |
| 2018-10-16 | UnivGen.constr_of_glob_univ -> Constr.mkRef | Gaëtan Gilbert |
| 2018-10-16 | Simplify fresh_foo_instance functions and pretyping of univ instance | Gaëtan Gilbert |
| 2018-07-03 | Remove unused env argument to fresh_sort_in_family | Gaëtan Gilbert |
| 2018-05-17 | Split off Universes functions dealing with generating new universes. | Gaëtan Gilbert |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |