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

...olable proof terms. As discussed in #454.
I think there is still a bit of discussion about the naming.


On Thu, Sep 4, 2014 at 8:23 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.
>
> Does that mean we should be using cbn instead of simpl everywhere? That's
> unfortunate, since it has a much less intuitive name.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17132322>.
>