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

...olable proof terms. As discussed in #454.
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?


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>.
>