coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Optimizing Int31 support in native compiler, by not tagging	Maxime Dénès	2014-04-09
*	Int31 decompilation in native compiler was still partial. Now fixed.	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
*	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès	2014-04-09
*	Int31 literals in native compiler.	Maxime Dénès	2014-04-09
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Native compiler: hash-consing of generated code and values.	mdenes	2013-03-25
*	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes	2013-02-11
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22