Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | 2014-05-06 | ||
* | - Fix abstract forgetting about new constraints. | 2014-05-06 | ||
* | - Fix handling of polymorphic inductive elimination schemes. | 2014-05-06 | ||
* | - Fix comparison of universes. | 2014-05-06 | ||
* | - Rename eq to equal in Univ, document new modules, set interfaces. | 2014-05-06 | ||
* | Initial work on reintroducing old-style polymorphism for compatibility (the s... | 2014-05-06 | ||
* | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | 2014-05-06 | ||
* | This commit adds full universe polymorphism and fast projections to Coq. | 2014-05-06 |