Use mattam82's version of Coq

Now we get slightly better universe polymorphism, eta for records, and
optimized record projections.