| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-10-02 | Loosen restrictions on mixing universe mono/polymorphism in sections | Gaëtan Gilbert | |
| We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |