aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/class.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* allow Prop as source for coercionsGravatar charguer2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 18:16:09 +0000