coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-05	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi
2014-08-05	STM: Classify Let as non asynchronous (Closes: #3486)	Enrico Tassi
2014-08-04	STM: VtQuery holds the id of the state it refers to	Carst Tankink
2014-07-01	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau
2014-06-06	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack
2014-05-15	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi
2014-05-15	Polymorphic Lemmas are like Defined ones for STM	Enrico Tassi
2014-05-06	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot
2014-05-06	Cleanup in constr, correct classification of polymorphic defs.	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-25	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot