aboutsummaryrefslogtreecommitdiff
path: root/engine/univGen.ml
AgeCommit message (Expand)Author
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
2018-10-16Clean UnivGen.fresh_instance APIGaëtan Gilbert
2018-10-16Simplify UnivGen.type_of_referenceGaëtan Gilbert
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:39:39 +0000