coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	[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-11-06
*	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	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
*	Fix bugs	Amin Timany	2017-06-16
*	Add subtyping inference for inductive types	Amin Timany	2017-06-16
*	Correct subtyping check for constructors	Amin Timany	2017-06-16
*	Fix typo in error message	Amin Timany	2017-06-16
*	Check subtyping of inductive types in Kernel	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-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Adding a local type-in-type flag in kernel declarations.	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
\|\
* \|	This is an attempt to clarify terminology in choosing variable names	Hugo Herbelin	2016-04-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\ \
\| * \|	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \|
\| * \|	Fixing bde12b70 about reporting ill-formed constructor.	Hugo Herbelin	2016-01-26
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Fixing e3cefca41b about supposingly simplifying primitive projections	Hugo Herbelin	2015-12-15
* \| \|	Slight simplification of the code of primitive projection (in relation	Hugo Herbelin	2015-12-05
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\| \|
\| * \|	Fixing fix c71aa6b to primitive projections.	Hugo Herbelin	2015-11-18
\| * \|	Slightly documenting code for building primitive projections.	Hugo Herbelin	2015-11-18
\| * \|	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \| \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\| \|
\| * \|	Dead code from the commit having introduced primitive projections (a4043608).	Hugo Herbelin	2015-11-10
\| * \|	Fixing a bug in reporting ill-formed constructor.	Hugo Herbelin	2015-11-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\| \|
\| * \|	Fixing a bug in reporting ill-formed inductive.	Hugo Herbelin	2015-10-22
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\| \|
\| * \|	Univs: inductives, remove unneeded test	Matthieu Sozeau	2015-10-14
* \| \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\| \|
\| * \|	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\| \|
\| * \|	Implementing Herbelin's fix for the "NonPar" bug	mlasson	2015-09-03
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\| \|