coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Store the {struct} inductive type in native fixpoint AST.	Pierre-Marie Pédrot	2018-07-13
*	Pass a proper environment to Nativelambda.lambda_of_constr.	Pierre-Marie Pédrot	2018-07-13
*	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert	2018-06-28
*	Merge PR #7772: [native_compute] Delay computations with toplevel match	Pierre-Marie Pédrot	2018-06-24
\|\
* \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
\| *	[native_compute] Delay computations with toplevel match	Maxime Dénès	2018-06-11
\|/
*	Use projection indices in native compilation rather than constant names.	Pierre-Marie Pédrot	2018-06-05
*	Fix #4714: Stack overflow with native compute	Maxime Dénès	2018-05-31
*	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-28
*	Unify pre_env and env	Maxime Dénès	2018-05-28
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Fix map iterator on nativelambda.	Maxime Dénès	2018-02-23
*	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
*	Fast environment lookup for rels.	Pierre-Marie Pédrot	2017-12-29
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove dead code in native compiler.	Maxime Dénès	2017-05-02
*	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
*	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
*	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
* \|	Avoid warnings about loop indices.	Guillaume Melquiond	2016-01-02
\|/
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	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-04-09
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Got rid of unused lazy flag in the native compiler.	Maxime Dénès	2013-12-29
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
*	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes	2013-07-06