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. |