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.
I don't like having explicit terms that require `match ... in ... return ...` annotations.  Is there a reason not to do these with tactics?