index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
declare.mli
Age
Commit message (
Expand
)
Author
2019-05-23
Fixing typos - Part 2
JPR
2019-05-19
Merge the definition of constants and private constants in the API.
Pierre-Marie Pédrot
2019-02-20
Merge PR #9529: Change Primitive message: "is registered" -> "is declared".
Vincent Laporte
2019-02-17
Separate variance and universe fields in inductives.
Gaëtan Gilbert
2019-02-08
Change Primitive message: "is registered" -> "is declared".
Gaëtan Gilbert
2019-02-04
Primitive integers
Maxime Dénès
2018-10-26
[libobject] Move object_name next to object definition.
Emilio Jesus Gallego Arias
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-22
Merge PR #7384: Split Universes
Pierre-Marie Pédrot
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-08
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2017-12-01
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-12-01
Proper nametab handling of global universe names
Matthieu Sozeau
2017-11-24
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-08-01
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-07-19
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
