| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix #6257: anomaly with Printing Projections and Context. |  Gaëtan Gilbert | 2018-03-30 |
| Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |