coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make eq_pattern_test/eq_test work up to the equivalence of primitive	Matthieu Sozeau	2014-09-24
*	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
*	Cleanup code related to the constraint solving, which sits now outside the	Matthieu Sozeau	2014-07-03
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	- 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