coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix substitution of universes which needlessly hashconsed existing universes.	Matthieu Sozeau	2014-06-10
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	- Add back some compatibility functions to avoid rewriting plugins.	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Fix issue #88: restrict_universe_context was wrongly forgetting about constra...	Matthieu Sozeau	2014-05-06
*	- Fix abstract forgetting about new constraints.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06