coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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