coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
*	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
*	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
*	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	2018-06-19
\|\
\| *	Remove Canary.	whitequark	2018-06-18
* \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/
*	Fix the checker by merely adapting the data structure.	Pierre-Marie Pédrot	2018-06-07
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
*	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
*	Add interfaces for checker and remove dead code.	Maxime Dénès	2018-01-10
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Merge PR #955: Do not hashcons universes beforehand	Maxime Dénès	2017-09-15
\|\
\| *	Do not hashcons universes beforehand.	Pierre-Marie Pédrot	2017-09-01
* \|	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
* \|	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
\|/
*	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	A short cleanup	Amin Timany	2017-06-16
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Correct coqchk reduction	Amin Timany	2017-06-16
*	Fixing the checker.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Fixing the checker.	Pierre-Marie Pédrot	2016-06-16
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Update cic.mli MD5 after header update.	Maxime Dénès	2016-01-20
* \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Univs: update checker	Matthieu Sozeau	2015-10-02
* \|	Updating checksum in checker (9c732a5cc continued).	Hugo Herbelin	2015-07-12
* \|	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
* \|	Checker: Fix bug #4282	Matthieu Sozeau	2015-07-07
\| *	Adjust checker after `Assume [Positive]`.	Arnaud Spiwack	2015-06-25
\|/
*	Splitting the library representation on disk in two.	Pierre-Marie Pédrot	2015-06-24
*	Exporting memory representation of STM tasks for votour.	Pierre-Marie Pédrot	2015-03-25
*	Fixing representation of dynamics in votour (again).	Pierre-Marie Pédrot	2015-03-24
*	Fix checker after addition of a universe context in with t := c constraints.	Matthieu Sozeau	2015-02-26
*	Update hash of cic.mli in checker/values.ml,	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	rename: vi -> vio	Enrico Tassi	2015-01-06
*	Vi2vo: fix handling of univ constraints coming from the body	Enrico Tassi	2014-12-23
*	Fixing checker representation of values.	Pierre-Marie Pédrot	2014-12-19
*	update md5 sums to make "make check" work	Enrico Tassi	2014-12-19
*	Fixing checker representation of universe lists.	Pierre-Marie Pédrot	2014-12-18