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.
Added:

> By giving `Funext` a field who's type is an axiom, we guarantee that we cannot construct a fresh instance of `Funext` without `admit`; there's no term of type `dummy_funext_type` floating around.  If we did not give `Funext` and fields, then we could accidentally manifest a `Funext` using, e.g., `constructor`, and then we wouldn't have a tag on the theorem that did this.