coq - The formal proof system

Age	Commit message (Expand)	Author
2016-10-22	Renamings to avoid confusion deprecating old names	Matthieu Sozeau
2016-07-04	congruence: Restrict refreshing to Set	Matthieu Sozeau
2016-07-04	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau
2016-01-20	Update copyright headers.	Maxime Dénès
2015-11-11	Fix bug #4293: ensure let-ins do not contain algebraic universes in	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-10-02	Work around issues with FO unification trying to unify terms of	Matthieu Sozeau
2014-09-19	Move the specific map_constr_with_binders_left_to_right	Matthieu Sozeau
2014-09-18	Fix constrMatching as well as change/e_contextually to allow	Matthieu Sozeau
2014-08-26	Make evarconv and unification able to handle eta for records in presence	Matthieu Sozeau
2014-08-25	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau
2014-07-30	Avoid introducing additional universes when doing pruning in evarsolve.	Matthieu Sozeau
2014-06-26	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau
2014-06-21	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau
2014-06-20	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau
2014-05-06	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-04-01	Propagating conversion_problem towards (postponed) evar/evar problems.	Hugo Herbelin
2013-10-22	Removing useless array-to-list and converse casts used in	ppedrot
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-02-28	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin
2013-02-17	Added propagation of evars unification failure reasons for better	herbelin
2013-02-10	Splitted Evarutil in two files	ppedrot