coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Safer VM interfaces	Maxime Dénès	2018-01-26
*	Merge PR #6506: Fast rel lookup	Maxime Dénès	2018-01-22
\|\
* \|	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
\| *	Fast environment lookup for rels.	Pierre-Marie Pédrot	2017-12-29
\|/
*	[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
*	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
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove unused open.	Guillaume Melquiond	2016-01-01
\|/ /
* /	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
*	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
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Modulification of identifier	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	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