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
2020-11-16
Syntax for specifying cumulative inductives
Gaëtan Gilbert
2020-11-13
[record] [ci] Overlay for elpi
Emilio Jesus Gallego Arias
2020-11-13
[record] Options API cleanup.
Emilio Jesus Gallego Arias
2020-11-13
[record] Cleanup of data structure and functions [1/2]
Emilio Jesus Gallego Arias
2020-07-09
Recordops: unify struc_typ summary record and libobject entry struc_tuple
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-07-01
[api] Reduce declare_kinds even more.
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-24
[api] Remove `polymorphic` type alias, use labels instead.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
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
