coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Less footguns in universe handling: remove subst_instance_context.	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
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
*	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-26
\|\
\| *	Fix bug #4876: critical bug in guard condition checker.	Matthieu Sozeau	2016-07-25
* \|	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
* \|	Moving the typing_flags to the environment.	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
\|\ \
\| * \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \| \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	This fix is probably not enough to justify that there are no problems with	Maxime Dénès	2016-03-04
* \| \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
* \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \|	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
\|/ / /
* \| \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \| \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \| \|	Contracting one extra beta-redex on the fly when typing branches of "match".	Hugo Herbelin	2015-12-05
* \| \|	A few renaming and simplification in inductive.ml.	Hugo Herbelin	2015-12-05
\|/ /
* \|	Univs: be more restrictive for template polymorphic constants: only	Matthieu Sozeau	2015-10-12
* \|	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
* \|	Univs/Inductive: fix typechecking of cases	Matthieu Sozeau	2015-07-15
* \|	Unused variables reported by OCaml.	Hugo Herbelin	2015-07-10
* \|	Kernel/Checker: Cleanup fixes of substitutions due to let-ins.	Matthieu Sozeau	2015-07-09
* \|	Template polymorphism: A bug-fix for Bug #4258	mlasson	2015-07-09
* \|	Univs: bug fix.	Matthieu Sozeau	2015-07-07
\| *	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
\|/
*	Fix my previous commit on ~polyprop	Pierre Letouzey	2015-05-12
*	Extraction: fix the detection of the "polyprop" situation	Pierre Letouzey	2015-05-12
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix some documentation typos.	Guillaume Melquiond	2015-01-06
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Fix generation of inductive elimination principle for primitive records.	Matthieu Sozeau	2014-09-10
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Relax a bit the guard condition.	Maxime Dénès	2014-08-06
*	One more optimization for guard checking of cofixpoints.	Maxime Dénès	2014-08-04
*	More optimization in guard checking.	Maxime Dénès	2014-08-04