Fix #6257: anomaly with Printing Projections and Context.

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.

0 files changed, 0 insertions, 0 deletions