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

...olable proof terms. As discussed in #454.
I'll make the changes if @andrejbauer is OK with the PR.


On Fri, Sep 5, 2014 at 5:58 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/PathGroupoids.v:
>
> > @@ -440,7 +440,7 @@ Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
> >    :
> >    (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
> >  Proof.
> > -  destruct q, s; simpl.
> > +  destruct q, s; cbn.
>
> Can we redefine simpl to mean cbn for us, at least until they've decided
> on the naming?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17180505>.
>