coq - The formal proof system

Age	Commit message (Expand)	Author
2019-10-05	Cleanup ComAssumption	Gaëtan Gilbert
2019-10-05	Move do_primitive from comassumption to its own module.	Gaëtan Gilbert
2019-08-19	[declare] Use `binding_kind` for implicit kind instead of boolean.	Emilio Jesus Gallego Arias
2019-08-08	Emit Feedback.AddedAxiom in Declare instead of higher layers	Gaëtan Gilbert
2019-07-01	[api] Refactor most of `Decl_kinds`	Emilio Jesus Gallego Arias
2019-06-24	Use named records instead of tuples where `polymorphic` used to be.	Gaëtan Gilbert
2019-06-24	[api] Remove `polymorphic` type alias, use labels instead.	Emilio Jesus Gallego Arias
2019-06-24	[api] Move `locality` from `library` to `vernac`.	Emilio Jesus Gallego Arias
2019-06-24	[lemmas] [proof] Split proof kinds into per-layer components.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-21	Remove definition-not-visible warning	Gaëtan Gilbert
2019-04-10	Functionalize env in type classes	Maxime Dénès
2019-03-27	[vernac] Thread proof state to declare_assumption for warning	Emilio Jesus Gallego Arias
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-05	Make Program a regular attribute	Maxime Dénès
2019-02-04	Primitive integers	Maxime Dénès
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-04-06	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias
2018-03-07	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès
2018-03-05	Allow universe declarations for [with Definition].	Gaëtan Gilbert
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-17	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias