index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
record.mli
Age
Commit message (
Expand
)
Author
2019-05-10
[Canonical structures] “not_canonical” annotation to field declarations
Vincent Laporte
2019-05-10
[Canonical structures] Some projections may not be canonical
Vincent Laporte
2019-05-07
[Record] Une a record to gather field declaration attributes
Vincent Laporte
2019-04-10
Remove calls to Global.env and Libobject from Recordops
Maxime Dénès
2019-02-17
Separate variance and universe fields in inductives.
Gaëtan Gilbert
2018-11-09
Remove remnants of polymorphic instance name registration.
Pierre-Marie Pédrot
2018-09-19
Fix #7754: universe declarations on mutual inductives
Gaëtan Gilbert
2018-09-13
Add explicit atribute for template polymorphism.
Gaëtan Gilbert
2018-06-29
Merge PR #7080: Swapping Context and Constr and defining declarations on cons...
Maxime Dénès
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-24
Handle mutual record at the vernac level.
Pierre-Marie Pédrot
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
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-19
record: restore API declare_projections (removed in e414c07e1)
Enrico Tassi
2017-12-10
[api] Remove kernel dependency on intf (Decl_kind)
Emilio Jesus Gallego Arias
2017-11-24
Register universe binders for record projections.
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-09-19
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-06-16
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
Extend definition of inductives to include subtyping info
Amin Timany
2017-03-24
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
