|
type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
|
