Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | 2014-06-06 | ||
* | poly: remove unused attribute to STM nodes and vernac classificaiton | 2014-05-15 | ||
* | Polymorphic Lemmas are like Defined ones for STM | 2014-05-15 | ||
* | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | 2014-05-06 | ||
* | Cleanup in constr, correct classification of polymorphic defs. | 2014-05-06 | ||
* | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | 2014-05-06 | ||
* | Rework handling of universes on top of the STM, allowing for delayed | 2014-05-06 | ||
* | This commit adds full universe polymorphism and fast projections to Coq. | 2014-05-06 | ||
* | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | 2014-04-25 |