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

...olable proof terms. As discussed in #454.
Could you be more specific? I don't fully appreciate the error message.

Also, a later push gives:
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. Integrate the remote changes (e.g.
hint: 'git pull ...') before pushing again.



On Thu, Sep 4, 2014 at 7:59 PM, Jason Gross <notifications@github.com>
wrote:

> In etc/coq-scripts:
>
> > @@ -1 +1 @@
> > -Subproject commit 6c4889941809dc83172755b576b5a9239c0571e6
> > +Subproject commit 4c7bd07be11e44ebd8322817ef6a316eac840307
>
> Yeah, that sounds about right. I mean, if you want to update coq-scripts
> to whatever the newest version is, feel free, but I'd prefer it done in its
> own commit and not bundled like this.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17130787>.
>