coq - The formal proof system

Age	Commit message (Expand)	Author
2017-06-16	Disable debug printing	Amin Timany
2017-06-16	Fix bugs and add an option for cumulativity	Amin Timany
2017-06-16	Fix bugs	Amin Timany
2017-05-03	Type@{_} should not produce a flexible algebraic universe.	Gaetan Gilbert
2017-05-03	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert
2015-12-02	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin
2015-10-07	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau
2015-07-07	Univs: bug fix.	Matthieu Sozeau
2015-06-28	Fix incompleteness of conversion used by evarconv	Matthieu Sozeau
2014-06-04	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-05-26	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau
2014-05-06	Fix restrict_universe_context removing some universes that do appear in the t...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2006-10-30	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin