Make `prod` a primitive record

Although we must work around three bugs ([bug #3481](https://coq.inria.fr/bugs/show_bug.cgi?id=3481), [bug #3507](https://coq.inria.fr/bugs/show_bug.cgi?id=3507), and [bug #3539](https://coq.inria.fr/bugs/show_bug.cgi?id=3539)), the work-arounds are relatively minor, so I'm in favor of merging this rather than waiting for @mattam82 to fix those bugs.  (For example, I want to prove the functor version of `equiv_prod_assoc`, but if we don't have eta, then it needs to assume `Funext` and do annoying transports across `path_forall`.)

This gives us a hefty speed-up in categories/Comma/ProjectionFunctors (from 22s down to 9s).  (Making everything primitive records takes a lot more bug-working-around, but brings us an overall 2x speedup, approximately.)

Note: This updates the version of Coq that we depend on, so you may have to rebuild Coq to get this code to work.
Control over the proof term, in particular the ability to not have to destruct `z` and `z'`.  If we are doing things with tactics, either we need to do `change z with (fst z, snd z)` before we destruct `p`, or we need to `destruct z`.

However, it's now the case that `destruct` and `match` desugar to uses of primitive projections (when I wrote the code, `destruct` could break subject reduction, and I didn't bother to update it), so the proof term will be convertible with the one I give.

I'm fine with going back to tactic code instead, if you still think that's better and others agree, though I'd prefer not to make that pull request myself.