use primitive projections for our mixins

This hardly makes any difference in compile times (things get around 2 seconds faster, which may well be noise), but it also shouldn't harm, right?

Using them for the canonical structures themselves does not work, see https://github.com/coq/coq/pull/984