coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	COMMENT: Pre_env.env	Matej Kosik	2017-04-20
*	simplifying "Environ.push_named" function	Matej Kosik	2017-04-20
*	Revert "simplify: Environ.push_named"	Matej Košík	2017-04-10
*	simplify: Environ.push_named	Matej Kosik	2017-04-10
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\
\| *	Mapping named_context_val preserves sharing when possible.	Pierre-Marie Pédrot	2017-01-17
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	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
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\|/
*	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