coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Avoid introducing additional universes when doing pruning in evarsolve.	Matthieu Sozeau	2014-07-30
*	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau	2014-06-26
*	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau	2014-06-21
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Propagating conversion_problem towards (postponed) evar/evar problems.	Hugo Herbelin	2014-04-01
*	Removing useless array-to-list and converse casts used in	ppedrot	2013-10-22
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Splitted Evarutil in two files	ppedrot	2013-02-10