coq - The formal proof system

Age	Commit message (Expand)	Author
2015-10-15	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès
2015-07-10	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin
2015-01-12	Update headers.	Maxime Dénès
2014-08-03	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	- Fix comparison of universes.	Matthieu Sozeau
2014-05-06	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau
2014-05-06	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau