index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
univGen.mli
Age
Commit message (
Expand
)
Author
2021-04-14
Remove remote counter system
Gaëtan Gilbert
2020-12-04
Better primitive type support in custom string and numeral notations.
Fabian Kunze
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-01-28
Remove dead code in Globnames.
Pierre-Marie Pédrot
2019-10-16
[engine] Remove UnivGen.global_of_constr
Vincent Laporte
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-10
[api] Remove 8.10 deprecations.
Emilio Jesus Gallego Arias
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-19
Deprecating unused Engine.type_of_global.
Hugo Herbelin
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
Deprecate UnivGen.new_{univ,Type,Type_sort}
Gaëtan Gilbert
2018-10-16
Clean UnivGen.fresh_instance API
Gaëtan Gilbert
2018-10-16
Deprecate univ-dropping UnivGen.new_sort_in_family
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
