coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Mapping named_context_val preserves sharing when possible.	Pierre-Marie Pédrot	2017-01-17
*	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
*	Removing the now useless field env_named_val from named_context_val.	Pierre-Marie Pédrot	2016-09-09
*	More efficient implementation of map_named_val.	Pierre-Marie Pédrot	2016-09-09
*	Tentative fast-access named env	Pierre-Marie Pédrot	2016-09-09
*	Packing the named_context_val in a proper record and marking it private.	Pierre-Marie Pédrot	2016-09-09
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	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
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
*	Update headers.	Maxime Dénès	2015-01-12
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Revert "Decent error message when a constant is not found"	Enrico Tassi	2014-05-16
*	Decent error message when a constant is not found	Enrico Tassi	2014-05-16
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Using Hashmaps by default in constant and inductive maps. This changes fold and	Pierre-Marie Pédrot	2014-03-07
*	Inductive maps in Environ now use HMap.	Pierre-Marie Pédrot	2014-03-06
*	Using HMaps in Safe_env.environments, hopefully improving performances.	Pierre-Marie Pédrot	2014-03-05
*	Made Pre_env.lazy_val opaque.	Pierre-Marie Pédrot	2014-02-11
*	STM: additional fix for STM + vm_compute	Enrico Tassi	2014-01-07
*	STM: fix worker crash when doing vm_compute	Enrico Tassi	2014-01-06
*	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
*	Revert "Fast lookup_named in environments, based on maps instead of lists."	ppedrot	2013-11-15
*	Fast lookup_named in environments, based on maps instead of lists.	ppedrot	2013-11-13
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Allocation-friendly version of [Pre_env.push_named].	ppedrot	2013-10-29
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Modulification of identifier	ppedrot	2012-12-14
*	More monomorphizations	ppedrot	2012-11-13
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17