coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	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
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25
* \|	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| *	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06