Using the standard (type class based) transitivity tactic for more contr...

...olable proof terms. As discussed in #454.
Actually, @spitters, the way to get `git push` to use spitter/HoTT rather
than HoTT/HoTT is to change "remote = upstream" to "remote = origin" (or
whatever remote you use) in `.git/config`.

On Thu, Sep 4, 2014 at 11:15 AM, Bas Spitters <notifications@github.com>
wrote:

> In etc/coq-scripts:
>
> > @@ -1 +1 @@
> > -Subproject commit 6c4889941809dc83172755b576b5a9239c0571e6
> > +Subproject commit 4c7bd07be11e44ebd8322817ef6a316eac840307
>
> That seems to have worked. To prevent problems in the future, my `git
> push` now pushes to HoTT/HoTT instead of spitters/HoTT, I am sure I need to
> change something in config. Do you know what?
> … <#14841e190e45fbeb_>
> On Thu, Sep 4, 2014 at 8:06 PM, Jason Gross <notifications@github.com>
> wrote: In etc/coq-scripts: > @@ -1 +1 @@ > -Subproject commit
> 6c4889941809dc83172755b576b5a9239c0571e6 > +Subproject commit
> 4c7bd07be11e44ebd8322817ef6a316eac840307 It's not an error message; it's
> feedback on what the command is doing. It's saying "you used to be at
> commit 4c... which had description 'Fix an off-by-one-error', and now
> you've moved to commit 6c... with description 'Fix a typo'". You'll need to
> push -f because you commit --amended. — Reply to this email directly or
> view it on GitHub <https://github.com/HoTT/HoTT/pull/459/files#r17131277>.
>
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17131881>.
>