Move to trunk

The day we've all been waiting for has arrived.  The days of faster Coq'ing are upon us.  This pull request updates the library with the last remaining changes necessary to move to trunk.

If you make use of the bundled submodule for building Coq, It is very likely that you will have to run `./autogen.sh` after pulling (and, of course, re-build Coq).

Since the `Local` keyword has been replaced by the `Private` keyword, this code will no longer compile with HoTT/coq.  If we want to, we can add a tag to the HoTT/coq version for posterity.

In this pull request, I've used an `admit` so as not to depend on #407.  I'm happy to have either this or #407 merged first (with a slight preference for #407 first), and will rebase the other one to be compatible.

Once this is merged, and the troubles with primitive projections are fixed, I'll submit a pull request to take advantage of primitive projections and eta.

This will allow us to deal with #335 and #402.  This closes #301.
Done.  Here's the elaborated comment:

> We use a dummy class and an axiom to get universe polymorphism of `Funext` while still tracking its uses.  Coq's universe polymorphism is parametric; in all definitions, all universes are quantified over before any other variables.  It's impossible to state a theorem like `(forall i : Level, P i) -> Q` (e.g., "if `C` has all limits of all sizes, then `C` is a preorder" isn't statable).¹  By making `isequiv_apD10` an `Axiom` rather than a per-theorem hypothesis, we can use it at multiple incompatible universe levels.  By only allowing use of the axiom when we have a `Funext` in the context, we can still track what theorems depend on it (because their type will mention `Funext`).
>
> ¹ That's not technically true; it might be possible to get non-parametric universe polymorphism using `Module`s and (`Module`) Functors; we can use functors to quantify over a `Module Type` which requires a polymorphic proof of a given hypothesis, and then use that hypothesis polymorphically in any theorem we prove in our new `Module` Functor.  But that is far beyond the scope of this file.

(Except I used `*` rather than `¹` for the footnote in the source.)