aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/declare.mli
Commit message (Expand)AuthorAge
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
| * Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* | [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
|/
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* [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
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 15:05:00 +0000