coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
* \|	Experimenting documentation of the Vars.subst functions.	Hugo Herbelin	2015-12-05
\|/
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Cleanup substitution inside universe instances, only done through subst_fn now,	Matthieu Sozeau	2014-07-21
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Various fixes of universe polymorphism and projections when they're set.	Matthieu Sozeau	2014-05-06
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Optimization in kernel/vars.ml: directly allocate a fixed-size block in the	Pierre-Marie Pédrot	2014-02-20
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Optimizing Vars.replace_vars	ppedrot	2013-10-23
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29