coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-09	Fix exponential behavior in native compiler with retroknowledge.	Maxime Dénès
2014-04-09	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-03-03	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
2013-12-30	Support for evars and metas in native compiler.	Maxime Dénès
2013-12-29	Got rid of unused lazy flag in the native compiler.	Maxime Dénès
2013-12-28	Removing native_name reference from constant_body.	Maxime Dénès
2013-07-06	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes
2013-03-25	Native compiler: hash-consing of generated code and values.	mdenes
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-03-05	More monomorphization.	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-11	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes