| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | In injection/inversion, consider all template-polymorphic types as injectable. |  Hugo Herbelin | 2017-11-28 |
| In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273). | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |