coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
\|/
*	Fix minor typo in native compiler.	Maxime Dénès	2015-10-28
*	Fix a critical bug in machine arithmetic for native compiler.	Maxime Dénès	2015-01-20
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix #3824. de Bruijn error in normalization of fixpoints.	Maxime Dénès	2014-11-23
*	Fixing incorrect printf format.	Pierre-Marie Pédrot	2014-06-02
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fix name of some Int31 operations in native compiler.	Maxime Dénès	2014-04-09
*	Machine arithmetic operations for native compiler.	Maxime Dénès	2014-04-09
*	Full support for int31 values in native compiler.	Maxime Dénès	2014-04-09
*	Partial support for open terms in int31.	Maxime Dénès	2014-04-09
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Native compiler: hash-consing of generated code and values.	mdenes	2013-03-25
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22