coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Work around issues with FO unification trying to unify terms of	Matthieu Sozeau	2014-10-02
*	Move the specific map_constr_with_binders_left_to_right	Matthieu Sozeau	2014-09-19
*	Fix constrMatching as well as change/e_contextually to allow	Matthieu Sozeau	2014-09-18
*	Make evarconv and unification able to handle eta for records in presence	Matthieu Sozeau	2014-08-26
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	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