coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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