coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	Fix restrict_universe_context to not remove useful constraints.	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	- Fix handling of polymorphic inductive elimination schemes.	Matthieu Sozeau
2014-05-06	- Fix comparison of universes.	Matthieu Sozeau
2014-05-06	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	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