coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
*	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
*	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 copyright headers.	Maxime Dénès	2016-01-20
* \|	Univs: update checker	Matthieu Sozeau	2015-10-02
* \|	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
*	Fix checker after addition of a universe context in with t := c constraints.	Matthieu Sozeau	2015-02-26
*	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
*	checker: Change in library on disk values, now using context_sets instead of	Matthieu Sozeau	2014-12-17
*	Update checker/values and cic due to changes in case_info and record_body.	Matthieu Sozeau	2014-12-17
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau	2014-09-06
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau	2014-09-05
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
*	Change in vo format : digest aren't Marshalled anymore	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Checker: vo validation checks the absence of Var/Evar/Meta	letouzey	2013-04-15
*	Checker: vo validation is now done in check.ml (and always)	letouzey	2013-04-15
*	Checker: empty sections hardcoded in cb and mind	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15