| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Implement module subtyping for polymorphic constants (errors on |  Matthieu Sozeau | 2014-10-02 |
| inductives). The implementation constant should have the a universe instance of the same length, we assume the universes are in the same order and we check that the definition does not add any constraints to the expected ones. This fixes bug #3670. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |