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.
I'd think it would be better to make dummy_funext_type non-polymorphic as
you don't need it, right?
-- Matthieu

Le mercredi 23 juillet 2014, Jason Gross <notifications@github.com> a
écrit :

> In theories/Overture.v:
>
> > @@ -347,8 +347,11 @@ Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_inst
> >  (** *** Function extensionality *)
> >
> >  (** The function extensionality axiom is formulated as a class. To use it in a theorem, just assume it with [`{Funext}], and then you can use [path_forall], defined below.  If you need function extensionality for a whole development, you can assume it for an entire Section with [Context `{Funext}].  *)
> > -Class Funext :=
> > -  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
> > +(** We use a dummy class and an axiom to get universe polymorphism of [Funext] while still tracking its uses. *)
> > +Axiom dummy_funext_type : Type.
>
> 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.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/415/files#r15293865>.
>


--